no goals
R : Type ?u.2956365
M✝ : Type ?u.2956368
inst✝¹⁹ : Semiring R
inst✝¹⁸ : AddCommMonoid M✝
inst✝¹⁷ : Module R M✝
R₁ : Type ?u.2956404
M₁ : Type ?u.2956407
inst✝¹⁶ : Ring R₁
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : Module R₁ M₁
R₂ : Type ?u.2957016
M₂ : Type ?u.2957019
inst✝¹³ : CommSemiring R₂
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R₂ M₂
R₃ : Type ?u.2957206
M₃ : Type ?u.2957209
inst✝¹⁰ : CommRing R₃
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R₃ M₃
V : Type ?u.2957797
K : Type ?u.2957800
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module K V
B : BilinForm R M✝
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Module A M₃
B₃ : BilinForm A M₃
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
M : Matrix ι ι A
⊢ Nondegenerate (↑toBilin' M) ↔ det M ≠ 0
rw [Matrix.nondegenerate_toBilin'_iff, Matrix.nondegenerate_iff_det_ne_zero]