@[implicit_reducible]

noncomputable instance instInvertibleTwoOfNeZero (k : Type u_1) [Field k] [NeZero 2] : Invertible 2

theorem QuadraticFormEquiv.associated_bilinForm_isSymm {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] (Q : QuadraticForm k V) : LinearMap.IsSymm (QuadraticMap.associated Q)

theorem QuadraticFormEquiv.quadForm_eq_associated_self {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] (Q : QuadraticForm k V) (x : V) : Q x = ((QuadraticMap.associated Q) x) x

theorem QuadraticFormEquiv.associated_eq_half_polar {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] (Q : QuadraticForm k V) (x y : V) : ((QuadraticMap.associated Q) x) y = ⅟2 * (Q (x + y) - Q x - Q y)

theorem QuadraticFormEquiv.associated_toQuadraticMap_eq {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] (Q : QuadraticForm k V) : (QuadraticMap.associated Q).toQuadraticMap = Q

theorem QuadraticFormEquiv.associated_of_symm_bilinForm {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (hB : LinearMap.IsSymm B) : QuadraticMap.associated (LinearMap.BilinMap.toQuadraticMap B) = B

theorem QuadraticFormEquiv.quadForm_add_expansion {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] (Q : QuadraticForm k V) (x y : V) : Q (x + y) = Q x + Q y + 2 * ((QuadraticMap.associated Q) x) y

noncomputable def QuadraticFormEquiv.matrixBilinEquiv {k : Type u_1} [Field k] {n : Type u_2} [Fintype n] [DecidableEq n] : Matrix n n k ≃ₗ[k] LinearMap.BilinMap k (n → k) k

noncomputable def QuadraticFormEquiv.bilinFormToMatrix {k : Type u_1} [Field k] {n : Type u_2} [Fintype n] [DecidableEq n] : LinearMap.BilinMap k (n → k) k ≃ₗ[k] Matrix n n k

theorem QuadraticFormEquiv.matrix_to_bilinForm_apply {k : Type u_1} [Field k] {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n k) (x y : n → k) : ((matrixBilinEquiv A) x) y = x ⬝ᵥ A.mulVec y

theorem QuadraticFormEquiv.toMatrix_toLinearMap₂ {k : Type u_1} [Field k] {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n k) : bilinFormToMatrix (matrixBilinEquiv A) = A

theorem QuadraticFormEquiv.toLinearMap₂_toMatrix {k : Type u_1} [Field k] {n : Type u_2} [Fintype n] [DecidableEq n] (B : LinearMap.BilinMap k (n → k) k) : matrixBilinEquiv (bilinFormToMatrix B) = B

noncomputable def QuadraticFormEquiv.matrixToQuadraticForm {k : Type u_1} [Field k] {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n k) : QuadraticForm k (n → k)

noncomputable def QuadraticFormEquiv.quadraticFormToMatrix {k : Type u_1} [Field k] [NeZero 2] {n : Type u_2} [Fintype n] [DecidableEq n] (Q : QuadraticForm k (n → k)) : Matrix n n k

theorem QuadraticFormEquiv.quadraticFormToMatrix_isSymm {k : Type u_1} [Field k] [NeZero 2] {n : Type u_2} [Fintype n] [DecidableEq n] (Q : QuadraticForm k (n → k)) : (QuadraticMap.toMatrix' Q).IsSymm

theorem QuadraticFormEquiv.bilinForm_symm_to_matrix_symm {k : Type u_1} [Field k] {n : Type u_2} [Fintype n] [DecidableEq n] (B : LinearMap.BilinForm k (n → k)) (hB : LinearMap.IsSymm B) : ((LinearMap.toMatrix₂' k) B).IsSymm

theorem QuadraticFormEquiv.matrix_symm_to_bilinForm_symm {k : Type u_1} [Field k] {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n k) (hA : A.IsSymm) : ((Matrix.toLinearMap₂' k) A).IsSymm

theorem QuadraticFormEquiv.equivalent_def {k : Type u_1} [CommSemiring k] {V : Type u_2} [AddCommMonoid V] [Module k V] (f g : QuadraticMap k V k) : f.Equivalent g ↔ Nonempty (f.IsometryEquiv g)

theorem QuadraticFormEquiv.equivalent_iff_exists_linearEquiv {k : Type u_1} [CommSemiring k] {V : Type u_2} [AddCommMonoid V] [Module k V] (f g : QuadraticMap k V k) : f.Equivalent g ↔ ∃ (T : V ≃ₗ[k] V), ∀ (v : V), g (T v) = f v

theorem QuadraticFormEquiv.isometryEquiv_map_app {k : Type u_1} [CommSemiring k] {V : Type u_2} [AddCommMonoid V] [Module k V] (f g : QuadraticMap k V k) (e : f.IsometryEquiv g) (v : V) : g (e v) = f v

theorem QuadraticFormEquiv.equivalent_refl {k : Type u_1} [CommSemiring k] {V : Type u_2} [AddCommMonoid V] [Module k V] (f : QuadraticMap k V k) : f.Equivalent f

theorem QuadraticFormEquiv.equivalent_symm {k : Type u_1} [CommSemiring k] {V : Type u_2} [AddCommMonoid V] [Module k V] {f g : QuadraticMap k V k} (h : f.Equivalent g) : g.Equivalent f

theorem QuadraticFormEquiv.equivalent_comm {k : Type u_1} [CommSemiring k] {V : Type u_2} [AddCommMonoid V] [Module k V] (f g : QuadraticMap k V k) : f.Equivalent g ↔ g.Equivalent f

theorem QuadraticFormEquiv.equivalent_trans {k : Type u_1} [CommSemiring k] {V : Type u_2} [AddCommMonoid V] [Module k V] {f g h : QuadraticMap k V k} (hfg : f.Equivalent g) (hgh : g.Equivalent h) : f.Equivalent h

theorem QuadraticFormEquiv.equivalent_isEquiv {k : Type u_1} [CommSemiring k] {V : Type u_2} [AddCommMonoid V] [Module k V] : Equivalence QuadraticMap.Equivalent

theorem QuadraticFormEquiv.weightedSumSquares_is_diagonal {k : Type u_1} [Field k] {n : ℕ} (w v : Fin n → k) : (QuadraticMap.weightedSumSquares k w) v = ∑ i : Fin n, w i * (v i * v i)

theorem QuadraticFormEquiv.diagonalization_via_orthogonal_basis {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] (Q : QuadraticForm k V) (v : Module.Basis (Fin (Module.finrank k V)) k V) (hv : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑v) : QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares k fun (i : Fin (Module.finrank k V)) => Q (v i))

theorem QuadraticFormEquiv.diagonalization_of_quadratic_forms {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (Q : QuadraticForm k V) : ∃ (w : Fin (Module.finrank k V) → k), QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares k w)

theorem QuadraticFormEquiv.exists_orthogonal_basis_for_quadForm {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (Q : QuadraticForm k V) : ∃ (v : Module.Basis (Fin (Module.finrank k V)) k V), LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑v

def QuadraticMap.Represents {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) (a : R) : Prop

theorem QuadraticMap.Represents.of_isometryEquiv {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : IsometryEquiv Q₁ Q₂) {a : R} (h : Represents Q₁ a) : Represents Q₂ a

theorem QuadraticMap.represents_iff_of_isometryEquiv {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : IsometryEquiv Q₁ Q₂) {a : R} : Represents Q₁ a ↔ Represents Q₂ a

theorem QuadraticMap.eval_smul_isotropic_add {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (Q : QuadraticForm k V) (v w : V) (x : k) (hv : Q v = 0) : Q (x • v + w) = Q w + x * polar (⇑Q) v w

theorem QuadraticMap.nondegenerate_represents_zero_represents_all {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (Q : QuadraticForm k V) (hnd : Nondegenerate) (hiso : Represents Q 0) (c : k) : Represents Q c

theorem QuadraticFormDef93.matrix_fullRank_iff_det_ne_zero {k : Type u_1} [Field k] {n : Type u_2} [Fintype n] [DecidableEq n] [Nonempty n] (A : Matrix n n k) : A.rank = Fintype.card n ↔ A.det ≠ 0

theorem QuadraticFormDef93.symmetric_dotProduct_zero_implies_mulVec_zero {k : Type u_1} [Field k] {n : Type u_2} [Fintype n] (M : Matrix n n k) (hM : M.IsSymm) (x : n → k) (h : ∀ (y : n → k), x ⬝ᵥ M.mulVec y = 0) : M.mulVec x = 0

noncomputable def QuadraticFormDef93.quadraticFormRank {k : Type u_1} [Field k] [NeZero 2] {n : Type u_2} [Fintype n] [DecidableEq n] (Q : QuadraticForm k (n → k)) : ℕ

def QuadraticFormDef93.quadraticFormIsNondegenerate {k : Type u_1} [Field k] [NeZero 2] {n : Type u_2} [Fintype n] [DecidableEq n] (Q : QuadraticForm k (n → k)) : Prop

theorem QuadraticFormDef93.quadraticForm_nondegenerate_iff_det_ne_zero {k : Type u_1} [Field k] [NeZero 2] {n : Type u_2} [Fintype n] [DecidableEq n] [Nonempty n] (Q : QuadraticForm k (n → k)) : quadraticFormIsNondegenerate Q ↔ (QuadraticMap.toMatrix' Q).det ≠ 0

theorem QuadraticFormDef93.toLinearMap₂'_toMatrix'_eq_associated {k : Type u_1} [Field k] [NeZero 2] {n : Type u_2} [Fintype n] [DecidableEq n] (Q : QuadraticForm k (n → k)) : (Matrix.toLinearMap₂' k) (QuadraticMap.toMatrix' Q) = QuadraticMap.associated Q

theorem QuadraticFormDef93.matrix_eq_associated_apply {k : Type u_1} [Field k] [NeZero 2] {n : Type u_2} [Fintype n] [DecidableEq n] (Q : QuadraticForm k (n → k)) (x y : n → k) : (((Matrix.toLinearMap₂' k) (QuadraticMap.toMatrix' Q)) x) y = ((QuadraticMap.associated Q) x) y

theorem QuadraticFormDef93.nondegenerate_associated_ne_zero {k : Type u_1} [Field k] [NeZero 2] {n : Type u_2} [Fintype n] [DecidableEq n] [Nonempty n] (Q : QuadraticForm k (n → k)) (hQ : quadraticFormIsNondegenerate Q) (x : n → k) (hx : x ≠ 0) : ∃ (y : n → k), ((QuadraticMap.associated Q) x) y ≠ 0

noncomputable def QuadraticFormDef94.sqMonoidHom (k : Type u_1) [Field k] : kˣ →* kˣ

noncomputable def QuadraticFormDef94.squaresSubgroup (k : Type u_1) [Field k] : Subgroup kˣ

def QuadraticFormDef94.SquareClassGroup (k : Type u_1) [Field k] : Type u_1

instance QuadraticFormDef94.squaresSubgroupNormal (k : Type u_1) [Field k] : (squaresSubgroup k).Normal

noncomputable def QuadraticFormDef94.toSquareClass (k : Type u_1) [Field k] : kˣ → SquareClassGroup k

theorem QuadraticFormDef94.toSquareClass_sq_mul (k : Type u_1) [Field k] (c a : kˣ) : toSquareClass k (c ^ 2 * a) = toSquareClass k a

noncomputable def QuadraticFormDef94.discrUnit (k : Type u_1) [Field k] [NeZero 2] {n : Type u_2} [Fintype n] [DecidableEq n] (Q : QuadraticMap k (n → k) k) (hQ : Q.discr ≠ 0) : kˣ

noncomputable def QuadraticFormDef94.discriminant (k : Type u_1) [Field k] [NeZero 2] {n : Type u_2} [Fintype n] [DecidableEq n] (Q : QuadraticMap k (n → k) k) (hQ : Q.discr ≠ 0) : SquareClassGroup k

theorem QuadraticFormDef94.linearEquiv_toMatrix'_det_ne_zero {k' : Type u_3} [Field k'] {m : Type u_4} [Fintype m] [DecidableEq m] (T : (m → k') ≃ₗ[k'] m → k') : (LinearMap.toMatrix' ↑T).det ≠ 0

theorem QuadraticFormDef94.discr_isometryEquiv_eq (k : Type u_1) [Field k] [NeZero 2] {n : Type u_2} [Fintype n] [DecidableEq n] {Q₁ Q₂ : QuadraticMap k (n → k) k} (e : Q₁.IsometryEquiv Q₂) : Q₁.discr = (LinearMap.toMatrix' ↑e.toLinearEquiv).det * (LinearMap.toMatrix' ↑e.toLinearEquiv).det * Q₂.discr

theorem QuadraticFormDef94.discriminant_preserved_by_isometryEquiv (k : Type u_1) [Field k] [NeZero 2] {n : Type u_2} [Fintype n] [DecidableEq n] {Q₁ Q₂ : QuadraticMap k (n → k) k} (e : Q₁.IsometryEquiv Q₂) (hQ₁ : Q₁.discr ≠ 0) (hQ₂ : Q₂.discr ≠ 0) : discriminant k Q₁ hQ₁ = discriminant k Q₂ hQ₂