Commit 2023-09-14 15:54 351962aa

View on Github →

feat(LinearAlgebra/QuadraticForm): add QuadraticForm.Isometry (#6984) Also use it to tidy the API of CliffordAlgebra.map.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

modified def CliffordAlgebra.map

modified theorem CliffordAlgebra.map_apply_ι

modified theorem CliffordAlgebra.map_comp_map

modified theorem CliffordAlgebra.map_comp_ι

modified theorem CliffordAlgebra.map_id

modified theorem CliffordAlgebra.ι_range_map_map

Modified Mathlib/LinearAlgebra/QuadraticForm/Dual.lean

modified def QuadraticForm.toDualProd

deleted theorem QuadraticForm.toDualProd_isometry

Created Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean

added theorem QuadraticForm.Isometry.coe_toLinearMap

added def QuadraticForm.Isometry.comp

added theorem QuadraticForm.Isometry.comp_assoc

added theorem QuadraticForm.Isometry.comp_id

added theorem QuadraticForm.Isometry.ext

added def QuadraticForm.Isometry.id

added theorem QuadraticForm.Isometry.id_comp

added theorem QuadraticForm.Isometry.map_app

added theorem QuadraticForm.Isometry.toLinearMap_comp

added theorem QuadraticForm.Isometry.toLinearMap_injective

added structure QuadraticForm.Isometry

Modified Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean

added def QuadraticForm.IsometryEquiv.toIsometry