Commit 2023-08-02 18:06 b9cabefa

View on Github →

refactor(LinearAlgebra/QuadraticForm): rename Isometry to IsometryEquiv (#6305) This is consistent with LinearIsometryEquiv vs LinearIsometry. The motivation is to make room for QuadraticForm.Isometry as the homomorphism.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

modified def CliffordAlgebra.equivOfIsometry

modified theorem CliffordAlgebra.equivOfIsometry_symm

modified theorem CliffordAlgebra.equivOfIsometry_trans

Modified Mathlib/LinearAlgebra/QuadraticForm/Complex.lean

Renamed Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean to Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean

modified def QuadraticForm.Equivalent

deleted theorem QuadraticForm.Isometry.coe_toLinearEquiv

deleted theorem QuadraticForm.Isometry.map_app

deleted def QuadraticForm.Isometry.refl

deleted def QuadraticForm.Isometry.symm

deleted def QuadraticForm.Isometry.trans

deleted structure QuadraticForm.Isometry

added theorem QuadraticForm.IsometryEquiv.coe_toLinearEquiv

added theorem QuadraticForm.IsometryEquiv.map_app

added def QuadraticForm.IsometryEquiv.refl

added def QuadraticForm.IsometryEquiv.symm

added def QuadraticForm.IsometryEquiv.trans

added structure QuadraticForm.IsometryEquiv

added def QuadraticForm.isometryEquivOfCompLinearEquiv

deleted def QuadraticForm.isometryOfCompLinearEquiv

Modified Mathlib/LinearAlgebra/QuadraticForm/Prod.lean

deleted def QuadraticForm.Isometry.pi

deleted def QuadraticForm.Isometry.prod

added def QuadraticForm.IsometryEquiv.pi

added def QuadraticForm.IsometryEquiv.prod

Modified Mathlib/LinearAlgebra/QuadraticForm/Real.lean