Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-10-19 13:16
ab701cad
View on Github →
feat(LinearAlgebra/QuadraticForm/Prod):
inl
,
inr
, and
single
are isometries (
#7723
)
Estimated changes
Modified
Mathlib/LinearAlgebra/QuadraticForm/Prod.lean
added
def
QuadraticForm.Isometry.inl
added
def
QuadraticForm.Isometry.inr
added
def
QuadraticForm.Isometry.single
added
theorem
QuadraticForm.pi_apply_single