Commit 2023-11-29 19:54 ae010c18

View on Github →

chore: introduce notation for AlternatingMap (#8697) Use M [Λ^ι]→ₗ[R] N for AlternatingMap R M N ι, similarly to the existing notation M [Λ^ι]→L[R] N for ContinuousAlternatingMap R M N ι.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Orientation.lean

Modified Mathlib/Analysis/InnerProductSpace/TwoDim.lean

Modified Mathlib/LinearAlgebra/Alternating/Basic.lean

modified theorem AlternatingMap.add_compLinearMap

modified def AlternatingMap.codRestrict

modified theorem AlternatingMap.coeFn_smul

modified theorem AlternatingMap.coe_alternatization

modified theorem AlternatingMap.coe_compLinearMap

modified theorem AlternatingMap.coe_inj

modified theorem AlternatingMap.coe_injective

modified theorem AlternatingMap.coe_neg

modified theorem AlternatingMap.coe_prod

modified theorem AlternatingMap.coe_zero

modified theorem AlternatingMap.compLinearEquiv_eq_zero_iff

modified def AlternatingMap.compLinearMap

modified theorem AlternatingMap.compLinearMap_apply

modified theorem AlternatingMap.compLinearMap_assoc

modified theorem AlternatingMap.compLinearMap_id

modified theorem AlternatingMap.compLinearMap_zero

modified theorem AlternatingMap.congr_arg

modified theorem AlternatingMap.congr_fun

modified def AlternatingMap.constLinearEquivOfIsEmpty

modified def AlternatingMap.constOfIsEmpty

modified def AlternatingMap.curryLeft

modified theorem AlternatingMap.curryLeft_add

modified theorem AlternatingMap.curryLeft_same

modified theorem AlternatingMap.curryLeft_smul

modified theorem AlternatingMap.curryLeft_zero

modified def AlternatingMap.domDomCongr

modified def AlternatingMap.domDomCongrEquiv

modified theorem AlternatingMap.domDomCongr_add

modified theorem AlternatingMap.domDomCongr_eq_iff

modified theorem AlternatingMap.domDomCongr_eq_zero_iff

modified theorem AlternatingMap.domDomCongr_refl

modified theorem AlternatingMap.domDomCongr_trans

modified theorem AlternatingMap.domDomCongr_zero

added def AlternatingMap.domDomCongrₗ

added theorem AlternatingMap.domDomCongrₗ_refl

added theorem AlternatingMap.domDomCongrₗ_toAddEquiv

deleted def AlternatingMap.domDomLcongr

deleted theorem AlternatingMap.domDomLcongr_refl

deleted theorem AlternatingMap.domDomLcongr_toAddEquiv

modified def AlternatingMap.domLCongr

modified theorem AlternatingMap.ext

modified theorem AlternatingMap.ext_iff

modified theorem AlternatingMap.map_vecCons_add

modified theorem AlternatingMap.map_vecCons_smul

modified def AlternatingMap.ofSubsingleton

modified def AlternatingMap.prod

modified theorem AlternatingMap.zero_apply

modified theorem AlternatingMap.zero_compLinearMap

modified theorem Basis.ext_alternating

modified theorem LinearMap.coe_compAlternatingMap

modified def LinearMap.compAlternatingMap

modified theorem LinearMap.compAlternatingMap_apply

modified theorem LinearMap.compAlternatingMap_codRestrict

modified theorem LinearMap.subtype_compAlternatingMap_codRestrict

modified def MultilinearMap.alternatization

Modified Mathlib/LinearAlgebra/Alternating/DomCoprod.lean

modified theorem AlternatingMap.domCoprod'_apply

modified def AlternatingMap.domCoprod.summand

modified theorem AlternatingMap.domCoprod.summand_add_swap_smul_eq_zero

modified theorem AlternatingMap.domCoprod.summand_eq_zero_of_smul_invariant

modified theorem AlternatingMap.domCoprod.summand_mk''

modified def AlternatingMap.domCoprod

modified theorem AlternatingMap.domCoprod_coe

Modified Mathlib/LinearAlgebra/Determinant.lean

modified theorem AlternatingMap.eq_smul_basis_det

Modified Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean

modified def ExteriorAlgebra.ιMulti

Modified Mathlib/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean

modified def ExteriorAlgebra.liftAlternating

modified def ExteriorAlgebra.liftAlternatingEquiv

modified theorem ExteriorAlgebra.liftAlternating_algebraMap

modified theorem ExteriorAlgebra.liftAlternating_apply_ιMulti

modified theorem ExteriorAlgebra.liftAlternating_comp

modified theorem ExteriorAlgebra.liftAlternating_comp_ιMulti

modified theorem ExteriorAlgebra.liftAlternating_one

modified theorem ExteriorAlgebra.liftAlternating_ι

modified theorem ExteriorAlgebra.liftAlternating_ι_mul

Modified Mathlib/LinearAlgebra/Matrix/Determinant.lean

modified def Matrix.detRowAlternating

Modified Mathlib/LinearAlgebra/Orientation.lean

modified theorem Orientation.map_apply

modified theorem Orientation.reindex_apply

Modified Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

modified theorem AlternatingMap.measure_parallelepiped

Modified Mathlib/Topology/Algebra/Module/Alternating.lean