Commit 2024-07-17 09:21 70b6992e

View on Github →

feat: Generalize quadratic isometries to quadratic maps (#14719) Also .prod and .pi, since these are heavily entangled with Isometry and IsometryEquiv. Follows on from #7569.

Estimated changes

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

modified theorem CliffordAlgebra.map_id

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Complex.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Dual.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean

deleted theorem QuadraticForm.Isometry.coe_toLinearMap

deleted def QuadraticForm.Isometry.comp

deleted theorem QuadraticForm.Isometry.comp_assoc

deleted theorem QuadraticForm.Isometry.comp_id

deleted theorem QuadraticForm.Isometry.ext

deleted def QuadraticForm.Isometry.id

deleted theorem QuadraticForm.Isometry.id_comp

deleted theorem QuadraticForm.Isometry.map_app

deleted def QuadraticForm.Isometry.ofEq

deleted theorem QuadraticForm.Isometry.ofEq_rfl

deleted theorem QuadraticForm.Isometry.toLinearMap_comp

deleted theorem QuadraticForm.Isometry.toLinearMap_injective

deleted structure QuadraticForm.Isometry

added theorem QuadraticMap.Isometry.coe_toLinearMap

added def QuadraticMap.Isometry.comp

added theorem QuadraticMap.Isometry.comp_assoc

added theorem QuadraticMap.Isometry.comp_id

added theorem QuadraticMap.Isometry.ext

added def QuadraticMap.Isometry.id

added theorem QuadraticMap.Isometry.id_comp

added theorem QuadraticMap.Isometry.map_app

added def QuadraticMap.Isometry.ofEq

added theorem QuadraticMap.Isometry.ofEq_rfl

added theorem QuadraticMap.Isometry.toLinearMap_comp

added theorem QuadraticMap.Isometry.toLinearMap_injective

added structure QuadraticMap.Isometry

Modified Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean

deleted theorem QuadraticForm.Equivalent.refl

deleted theorem QuadraticForm.Equivalent.symm

deleted theorem QuadraticForm.Equivalent.trans

deleted def QuadraticForm.Equivalent

deleted theorem QuadraticForm.IsometryEquiv.coe_toLinearEquiv

deleted theorem QuadraticForm.IsometryEquiv.map_app

deleted def QuadraticForm.IsometryEquiv.refl

deleted def QuadraticForm.IsometryEquiv.symm

deleted def QuadraticForm.IsometryEquiv.toIsometry

deleted def QuadraticForm.IsometryEquiv.trans

deleted structure QuadraticForm.IsometryEquiv

deleted def QuadraticForm.isometryEquivOfCompLinearEquiv

added theorem QuadraticMap.Equivalent.refl

added theorem QuadraticMap.Equivalent.symm

added theorem QuadraticMap.Equivalent.trans

added def QuadraticMap.Equivalent

added theorem QuadraticMap.IsometryEquiv.coe_toLinearEquiv

added theorem QuadraticMap.IsometryEquiv.map_app

added def QuadraticMap.IsometryEquiv.refl

added def QuadraticMap.IsometryEquiv.symm

added def QuadraticMap.IsometryEquiv.toIsometry

added def QuadraticMap.IsometryEquiv.trans

added structure QuadraticMap.IsometryEquiv

added def QuadraticMap.isometryEquivOfCompLinearEquiv

Modified Mathlib/LinearAlgebra/QuadraticForm/Prod.lean

deleted theorem QuadraticForm.Equivalent.pi

deleted theorem QuadraticForm.Equivalent.prod

deleted theorem QuadraticForm.IsOrtho.inl_inr

deleted theorem QuadraticForm.IsOrtho.inr_inl

deleted theorem QuadraticForm.IsOrtho.prod

deleted def QuadraticForm.Isometry.fst

deleted theorem QuadraticForm.Isometry.fst_comp_inl

deleted theorem QuadraticForm.Isometry.fst_comp_inr

deleted def QuadraticForm.Isometry.inl

deleted def QuadraticForm.Isometry.inr

deleted def QuadraticForm.Isometry.proj

deleted theorem QuadraticForm.Isometry.proj_comp_single_of_ne

deleted theorem QuadraticForm.Isometry.proj_comp_single_of_same

deleted def QuadraticForm.Isometry.single

deleted def QuadraticForm.Isometry.snd

deleted theorem QuadraticForm.Isometry.snd_comp_inl

deleted theorem QuadraticForm.Isometry.snd_comp_inr

deleted def QuadraticForm.IsometryEquiv.pi

deleted def QuadraticForm.IsometryEquiv.prod

deleted def QuadraticForm.IsometryEquiv.prodComm

deleted def QuadraticForm.IsometryEquiv.prodProdProdComm

deleted theorem QuadraticForm.PosDef.prod

deleted theorem QuadraticForm.Ring.associated_pi

deleted theorem QuadraticForm.Ring.polarBilin_pi

deleted theorem QuadraticForm.Ring.polar_pi

deleted theorem QuadraticForm.anisotropic_of_pi

deleted theorem QuadraticForm.anisotropic_of_prod

deleted theorem QuadraticForm.associated_prod

deleted theorem QuadraticForm.isOrtho_inl_inl_iff

deleted theorem QuadraticForm.isOrtho_inr_inr_iff

deleted theorem QuadraticForm.nonneg_pi_iff

deleted theorem QuadraticForm.nonneg_prod_iff

deleted def QuadraticForm.pi

deleted theorem QuadraticForm.pi_apply

deleted theorem QuadraticForm.pi_apply_single

deleted theorem QuadraticForm.polarBilin_prod

deleted theorem QuadraticForm.polar_prod

deleted theorem QuadraticForm.posDef_pi_iff

deleted theorem QuadraticForm.posDef_prod_iff

deleted def QuadraticForm.prod

added theorem QuadraticMap.Equivalent.pi

added theorem QuadraticMap.Equivalent.prod

added theorem QuadraticMap.IsOrtho.inl_inr

added theorem QuadraticMap.IsOrtho.inr_inl

added theorem QuadraticMap.IsOrtho.prod

added def QuadraticMap.Isometry.fst

added theorem QuadraticMap.Isometry.fst_comp_inl

added theorem QuadraticMap.Isometry.fst_comp_inr

added def QuadraticMap.Isometry.inl

added def QuadraticMap.Isometry.inr

added def QuadraticMap.Isometry.proj

added theorem QuadraticMap.Isometry.proj_comp_single_of_ne

added theorem QuadraticMap.Isometry.proj_comp_single_of_same

added def QuadraticMap.Isometry.single

added def QuadraticMap.Isometry.snd

added theorem QuadraticMap.Isometry.snd_comp_inl

added theorem QuadraticMap.Isometry.snd_comp_inr

added def QuadraticMap.IsometryEquiv.pi

added def QuadraticMap.IsometryEquiv.prod

added def QuadraticMap.IsometryEquiv.prodComm

added def QuadraticMap.IsometryEquiv.prodProdProdComm

added theorem QuadraticMap.PosDef.prod

added theorem QuadraticMap.Ring.associated_pi

added theorem QuadraticMap.Ring.polarBilin_pi

added theorem QuadraticMap.Ring.polar_pi

added theorem QuadraticMap.anisotropic_of_pi

added theorem QuadraticMap.anisotropic_of_prod

added theorem QuadraticMap.associated_prod

added theorem QuadraticMap.isOrtho_inl_inl_iff

added theorem QuadraticMap.isOrtho_inr_inr_iff

added theorem QuadraticMap.nonneg_pi_iff

added theorem QuadraticMap.nonneg_prod_iff

added def QuadraticMap.pi

added theorem QuadraticMap.pi_apply

added theorem QuadraticMap.pi_apply_single

added theorem QuadraticMap.polarBilin_prod

added theorem QuadraticMap.polar_prod

added theorem QuadraticMap.posDef_pi_iff

added theorem QuadraticMap.posDef_prod_iff

added def QuadraticMap.prod

Modified Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Real.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/TensorProduct/Isometries.lean

deleted def QuadraticForm.Isometry.tmul

deleted theorem QuadraticForm.Isometry.tmul_apply

added def QuadraticMap.Isometry.tmul

added theorem QuadraticMap.Isometry.tmul_apply