pub fn prove_inverse(
ctx: &Context,
a: &[Vec<Rational>],
) -> Option<(Vec<Vec<Rational>>, Vec<Vec<Term>>)>Expand description
Invert A and PROVE it in the kernel: every entry of A·A⁻¹ = I is a dot-product proof
Aᵢ·(A⁻¹)ⱼ = Iᵢⱼ (the off-diagonal = 0 identities are proven too). None iff singular / past i64.