Commit 2024-02-13 19:40 7b0f450d

View on Github →

feat: add fst and snd for QuadraticForm.Isometry (#10381) Also adds proj for the Pi variation, along with Isometry.ofEq to make it possible to state the theorems for the Pi type.

Estimated changes

Modified Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean

added def QuadraticForm.Isometry.ofEq

added theorem QuadraticForm.Isometry.ofEq_rfl

Modified Mathlib/LinearAlgebra/QuadraticForm/Prod.lean

added def QuadraticForm.Isometry.fst

added theorem QuadraticForm.Isometry.fst_comp_inl

added theorem QuadraticForm.Isometry.fst_comp_inr

added def QuadraticForm.Isometry.proj

added theorem QuadraticForm.Isometry.proj_comp_single_of_ne

added theorem QuadraticForm.Isometry.proj_comp_single_of_same

added def QuadraticForm.Isometry.snd

added theorem QuadraticForm.Isometry.snd_comp_inl

added theorem QuadraticForm.Isometry.snd_comp_inr