Commit 2024-03-01 17:50 008d6e96

View on Github →

fix: denote alternating map by ⋀, not Λ (#11064) That is, \bigwedge, not \Lambda

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

modified def AlternatingMap.domDomCongrₗ

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/Basic.lean

modified def ContinuousAlternatingMap.applyAddHom

modified def ContinuousAlternatingMap.codRestrict

modified theorem ContinuousAlternatingMap.coe_restrictScalars

modified theorem ContinuousAlternatingMap.coe_smul

modified theorem ContinuousAlternatingMap.coe_zero

modified def ContinuousAlternatingMap.compContinuousLinearMap

modified theorem ContinuousAlternatingMap.compContinuousLinearMap_apply

modified def ContinuousAlternatingMap.compContinuousLinearMapₗ

modified def ContinuousAlternatingMap.constOfIsEmpty

modified theorem ContinuousAlternatingMap.ext

modified theorem ContinuousAlternatingMap.ext_iff

modified def ContinuousAlternatingMap.prod

modified def ContinuousAlternatingMap.restrictScalars

modified def ContinuousAlternatingMap.smulRight

modified theorem ContinuousAlternatingMap.smul_apply

modified theorem ContinuousAlternatingMap.sum_apply

modified theorem ContinuousAlternatingMap.toAlternatingMap_add

modified theorem ContinuousAlternatingMap.toAlternatingMap_smul

modified theorem ContinuousAlternatingMap.toAlternatingMap_zero

modified theorem ContinuousAlternatingMap.toContinuousMultilinearMap_add

modified theorem ContinuousAlternatingMap.toContinuousMultilinearMap_smul

modified theorem ContinuousAlternatingMap.toContinuousMultilinearMap_zero

modified def ContinuousAlternatingMap.toMultilinearAddHom

modified def ContinuousLinearMap.compContinuousAlternatingMap

modified def ContinuousMultilinearMap.alternatization