Basic

📁 Source: Mathlib/LinearAlgebra/Alternating/Basic.lean

Statistics

Metric	Count
Definitions AlternatingMap, codRestrict, compLinearMap, constLinearEquivOfIsEmpty, constOfIsEmpty, domDomCongr, domDomCongrEquiv, domDomCongrₗ, domLCongr, instAdd, instAddCommGroup, instAddCommMonoid, instCoe, instDistribMulAction, instFunLike, instInhabited, instModule, instNeg, instSMul, instSub, instZero, ofSubsingleton, pi, prod, smulRight, toMultilinearMap, toMultilinearMapLM, uniqueOfCommRing, alternatingMapCongrRight, compAlternatingMap, compAlternatingMapₗ, alternatization, «term_[⋀^_]→ₗ[_]_»	33
Theorems add_apply, add_compLinearMap, codRestrict_apply_coe, coeFn_smul, coe_add, coe_alternatization, coe_compLinearMap, coe_domDomCongr, coe_inj, coe_injective, coe_mk, coe_multilinearMap, coe_multilinearMap_injective, coe_multilinearMap_mk, coe_neg, coe_pi, coe_prod, coe_smul, coe_smulRight, coe_sub, coe_zero, compLinearEquiv_eq_zero_iff, compLinearMap_apply, compLinearMap_assoc, compLinearMap_id, compLinearMap_inj, compLinearMap_injective, compLinearMap_zero, congr_arg, congr_fun, constLinearEquivOfIsEmpty_apply, constLinearEquivOfIsEmpty_symm_apply, constOfIsEmpty_apply, domDomCongrEquiv_apply, domDomCongrEquiv_symm_apply, domDomCongr_add, domDomCongr_apply, domDomCongr_eq_iff, domDomCongr_eq_zero_iff, domDomCongr_perm, domDomCongr_refl, domDomCongr_smul, domDomCongr_trans, domDomCongr_zero, domDomCongrₗ_apply, domDomCongrₗ_refl, domDomCongrₗ_symm_apply, domDomCongrₗ_toAddEquiv, domLCongr_apply, domLCongr_refl, domLCongr_symm, domLCongr_trans, ext, ext_iff, ext_ring, ext_ring_iff, instIsCentralScalar, instIsTorsionFree, instSMulCommClass, map_add_swap, map_congr_perm, map_coord_zero, map_eq_zero_of_eq, map_eq_zero_of_eq', map_eq_zero_of_not_injective, map_linearDependent, map_perm, map_swap, map_swap_add, map_update_add, map_update_neg, map_update_self, map_update_smul, map_update_sub, map_update_sum, map_update_update, map_update_zero, map_vecCons_add, map_vecCons_smul, map_zero, mk_zero, neg_apply, ofSubsingleton_apply_apply, ofSubsingleton_symm_apply_apply, pi_apply, prod_apply, smulRight_apply, smul_apply, sub_apply, toFun_eq_coe, toMultilinearMapLM_apply, zero_apply, zero_compLinearMap, alternatingMapCongrRight_apply_apply, alternatingMapCongrRight_symm_apply_apply, add_compAlternatingMap, coe_compAlternatingMap, compAlternatingMap_add, compAlternatingMap_apply, compAlternatingMap_codRestrict, compAlternatingMap_smul, compAlternatingMap_zero, compAlternatingMapₗ_apply, compMultilinearMap_alternatization, smulRight_eq_comp, smul_compAlternatingMap, subtype_compAlternatingMap_codRestrict, zero_compAlternatingMap, ext_alternating, alternatization_apply, alternatization_coe, alternatization_def	112
Total	145

AlternatingMap

Definitions

Name	Category	Theorems
codRestrict 📖	CompOp	3 math math: LinearMap.subtype_compAlternatingMap_codRestrict, LinearMap.compAlternatingMap_codRestrict, codRestrict_apply_coe
compLinearMap 📖	CompOp	17 math math: exteriorPower.alternatingMapLinearEquiv_symm_map, zero_compLinearMap, ExteriorAlgebra.map_comp_ιMulti, compLinearMap_id, compLinearMap_injective, Module.Basis.det_map', exteriorPower.map_comp_ιMulti, compLinearMap_zero, compLinearMap_assoc, compLinearMap_inj, coe_compLinearMap, curryLeft_compLinearMap, Orientation.map_apply, compLinearMap_apply, domLCongr_apply, compLinearEquiv_eq_zero_iff, add_compLinearMap
constLinearEquivOfIsEmpty 📖	CompOp	4 math math: constLinearEquivOfIsEmpty_symm_apply, constLinearEquivOfIsEmpty_apply, Orientation.volumeForm_zero_pos, Orientation.volumeForm_zero_neg
constOfIsEmpty 📖	CompOp	4 math math: constLinearEquivOfIsEmpty_apply, ContinuousAlternatingMap.constOfIsEmpty_toAlternatingMap, Module.Basis.det_isEmpty, constOfIsEmpty_apply
domDomCongr 📖	CompOp	16 math math: domDomCongr_zero, domDomCongr_eq_zero_iff, Module.Basis.det_reindex', domDomCongr_smul, coe_domDomCongr, domDomCongrEquiv_apply, domDomCongr_eq_iff, domDomCongr_refl, domDomCongr_add, Orientation.reindex_apply, domDomCongr_perm, domDomCongrₗ_symm_apply, domDomCongr_trans, domDomCongrₗ_apply, domDomCongr_apply, domDomCongrEquiv_symm_apply
domDomCongrEquiv 📖	CompOp	3 math math: domDomCongrEquiv_apply, domDomCongrₗ_toAddEquiv, domDomCongrEquiv_symm_apply
domDomCongrₗ 📖	CompOp	4 math math: domDomCongrₗ_refl, domDomCongrₗ_toAddEquiv, domDomCongrₗ_symm_apply, domDomCongrₗ_apply
domLCongr 📖	CompOp	4 math math: domLCongr_refl, domLCongr_trans, domLCongr_apply, domLCongr_symm
instAdd 📖	CompOp	13 math math: add_apply, alternatizeUncurryFin_add, LinearMap.compAlternatingMap_add, domDomCongrEquiv_apply, domDomCongr_add, domDomCongrₗ_toAddEquiv, LinearMap.add_compAlternatingMap, uncurryFin_add, coe_add, ContinuousAlternatingMap.toAlternatingMap_add, domDomCongrEquiv_symm_apply, add_compLinearMap, curryLeft_add
instAddCommGroup 📖	CompOp	30 math math: Orientation.ne_iff_eq_neg, Orientation.volumeForm_neg_orientation, Orientation.eq_or_eq_neg, uncurryFin_curryLeft, Orientation.map_eq_neg_iff_det_neg, Orientation.areaForm_neg_orientation, Orientation.reindex_neg, LinearMap.compMultilinearMap_alternatization, MultilinearMap.domCoprod_alternization_coe, Module.Basis.orientation_eq_or_eq_neg, MultilinearMap.domCoprod_alternization_eq, Orientation.kahler_neg_orientation, Module.Basis.orientation_ne_iff_eq_neg, Orientation.rotation_neg_orientation_eq_neg, alternatizeUncurryFin_curryLeft, Module.Basis.orientation_comp_linearEquiv_eq_neg_iff_det_neg, MultilinearMap.alternatization_apply, coe_alternatization, Orientation.map_neg, MultilinearMap.domCoprod_alternization, Orientation.rightAngleRotation_trans_neg_orientation, ContinuousMultilinearMap.alternatization_apply_toAlternatingMap, Orientation.volumeForm_zero_neg, MultilinearMap.alternatization_coe, domDomCongr_perm, Module.Basis.orientation_neg_single, Orientation.eq_or_eq_neg_of_isEmpty, Orientation.oangle_neg_orientation_eq_neg, Orientation.rightAngleRotation_neg_orientation, MultilinearMap.alternatization_def
instAddCommMonoid 📖	CompOp	60 math math: domLCongr_refl, constLinearEquivOfIsEmpty_symm_apply, constLinearEquivOfIsEmpty_apply, domDomCongrₗ_refl, ExteriorAlgebra.liftAlternating_ι_mul, ContinuousAlternatingMap.toAlternatingMapLinear_apply, exteriorPower.alternatingMapLinearEquiv_ιMulti, ExteriorAlgebra.liftAlternating_comp, instIsTorsionFree, ContinuousAlternatingMap.toAlternatingMap_curryLeft, exteriorPower.alternatingMapLinearEquiv_symm_map, alternatizeUncurryFin_apply, ExteriorAlgebra.liftAlternatingEquiv_symm_apply, Orientation.volumeForm_zero_pos, alternatizeUncurryFin_add, ExteriorAlgebra.liftAlternating_ιMulti, ExteriorAlgebra.liftAlternatingEquiv_apply, curryLeft_apply_apply, ExteriorAlgebra.liftAlternating_apply_ιMulti, Orientation.map_eq_det_inv_smul, curryLeft_apply_toMultilinearMap, alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply, ExteriorAlgebra.liftAlternating_one, domCoprod'_apply, exteriorPower.alternatingMapLinearEquiv_apply_ιMulti, curryLeft_zero, exteriorPower.alternatingMapLinearEquiv_comp_ιMulti, ContinuousAlternatingMap.toAlternatingMap_alternatizeUncurryFin, LinearEquiv.alternatingMapCongrRight_apply_apply, curryLeftLinearMap_apply, exteriorPower.alternatingMapLinearEquiv_comp, curryLeft_smul, domDomCongrₗ_toAddEquiv, uncurryFin_smul, ExteriorAlgebra.liftAlternating_comp_ιMulti, Module.Basis.map_orientation_eq_det_inv_smul, curryLeft_compAlternatingMap, Orientation.volumeForm_zero_neg, uncurryFin_add, ExteriorAlgebra.liftAlternating_algebraMap, Module.Basis.orientation_unitsSMul, exteriorPower.alternatingMapLinearEquiv_symm_apply, Orientation.reindex_apply, curryLeft_compLinearMap, domDomCongrₗ_symm_apply, Orientation.map_apply, uncurryFin_apply, domLCongr_trans, domLCongr_apply, ExteriorAlgebra.ιMulti_succ_curryLeft, domDomCongrₗ_apply, alternatizeUncurryFin_smul, LinearEquiv.alternatingMapCongrRight_symm_apply_apply, alternatizeUncurryFinLM_apply, domLCongr_symm, LinearMap.compAlternatingMapₗ_apply, ExteriorAlgebra.liftAlternating_ι, toMultilinearMapLM_apply, curryLeft_add, curryLeft_same
instCoe 📖	CompOp	—
instDistribMulAction 📖	CompOp	6 math math: Orientation.map_eq_det_inv_smul, curryLeft_smul, uncurryFin_smul, Module.Basis.map_orientation_eq_det_inv_smul, Module.Basis.orientation_unitsSMul, alternatizeUncurryFin_smul
instFunLike 📖	CompOp	143 math math: sub_apply, Module.Basis.det_comp_basis, add_apply, LinearMap.coe_compAlternatingMap, LinearMap.compAlternatingMap_apply, constLinearEquivOfIsEmpty_symm_apply, map_vecCons_smul, map_perm, map_linearDependent, congr_fun, ExteriorAlgebra.ιMulti_span_fixedDegree, smulRight_apply, OrthonormalBasis.det_to_matrix_orthonormalBasis_of_same_orientation, Module.Basis.isUnit_det, OrthonormalBasis.det_to_matrix_orthonormalBasis_of_opposite_orientation, map_update_smul, congr_arg, smul_apply, Orientation.volumeForm_map, neg_apply, Module.Basis.det_isUnitSMul, Orientation.abs_volumeForm_apply_of_orthonormal, exteriorPower.ιMulti_span_of_span, map_basis_eq_zero_iff, ExteriorAlgebra.ιMulti_succ_apply, ext_ring_iff, ExteriorAlgebra.ιMulti_span, Orientation.areaForm_to_volumeForm, ExteriorAlgebra.ιMulti_zero_apply, AddSubgroup.index_eq_natAbs_det, alternatizeUncurryFin_apply, zero_apply, Module.Basis.orientation_eq_iff_det_pos, ZSpan.measureReal_fundamentalDomain, map_congr_perm, map_update_add, curryLeft_apply_apply, exteriorPower.presentation.relationsSolutionEquiv_symm_apply_var, NumberField.det_basisOfFractionalIdeal_eq_absNorm, ZSpan.measure_fundamentalDomain, Module.Basis.smul_det, constOfIsEmpty_apply, ExteriorAlgebra.ιMulti_range, exteriorPower.presentation.relationsSolutionEquiv_apply_apply, Orientation.abs_volumeForm_apply_of_pairwise_orthogonal, ExteriorAlgebra.liftAlternating_apply_ιMulti, exteriorPower.ιMulti_span_fixedDegree_of_span_eq_top, neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq, map_update_zero, exteriorPower.ιMulti_apply_coe, Module.Basis.det_reindex_symm, ofSubsingleton_apply_apply, map_eq_zero_of_not_injective, coe_mk, MeasureTheory.Measure.addHaar_parallelepiped, alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply, ExteriorAlgebra.liftAlternating_one, map_update_sum, coe_inj, map_update_update, AddSubgroup.relIndex_eq_abs_det, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, exteriorPower.alternatingMapLinearEquiv_apply_ιMulti, OrthonormalBasis.det_to_matrix_orthonormalBasis, exteriorPower.ιMultiDual_apply_ιMulti, exteriorPower.pairingDual_ιMulti_ιMulti, Module.Basis.det_reindex, exteriorPower.oneEquiv_symm_apply, map_eq_zero_of_eq, InnerProductSpace.gramSchmidtOrthonormalBasis_det, eq_smul_basis_det, coe_injective, LinearEquiv.alternatingMapCongrRight_apply_apply, exteriorPower.pairingDual_apply_apply_eq_one, ZLattice.covolume_eq_det_mul_measureReal, map_update_neg, Module.Basis.det_comp, MultilinearMap.alternatization_apply, map_vecCons_add, ExteriorAlgebra.ιMulti_apply, ContinuousAlternatingMap.range_toAlternatingMap, exteriorPower.alternatingMapToDual_apply_ιMulti, Module.Basis.abs_det_adjustToOrientation, Module.Basis.det_self, Module.Basis.det_basis, map_update_sub, Module.Basis.det_inv, exteriorPower.zeroEquiv_ιMulti, prod_apply, coeFn_smul, Orientation.volumeForm_robust', ext_iff, ofSubsingleton_symm_apply_apply, coe_multilinearMap, map_update_self, map_zero, toFun_eq_coe, ExteriorAlgebra.map_apply_ιMulti, LinearMap.compAlternatingMap_codRestrict, measure_def, exteriorPower.pairingDual_apply_apply_eq_one_zero, Orientation.volumeForm_apply_le, FractionalIdeal.abs_det_basis_change, Module.Basis.det_mul_det, ExteriorAlgebra.liftAlternating_algebraMap, map_swap, exteriorPower.alternatingMapLinearEquiv_symm_apply, measure_parallelepiped, coe_compLinearMap, exteriorPower.map_apply_ιMulti, map_swap_add, uncurryFin_apply, map_add_swap, compLinearMap_apply, neg_one_pow_smul_map_insertNth, AddSubgroup.relIndex_eq_natAbs_det, map_insertNth, exteriorPower.presentation_var, Module.Basis.det_unitsSMul_self, Module.Basis.det_smul_mk_coord_eq_det_update, pi_apply, LinearEquiv.alternatingMapCongrRight_symm_apply_apply, ContinuousAlternatingMap.coe_toAlternatingMap, OrthonormalBasis.det_to_matrix_orthonormalBasis_real, exteriorPower.ιMulti_span_fixedDegree, domCoprod_apply, exteriorPower.oneEquiv_ιMulti, exteriorPower.ιMulti_span, exteriorPower.toTensorPower_apply_ιMulti, Module.Basis.det_map, Ideal.natAbs_det_basis_change, OrthonormalBasis.abs_det_adjustToOrientation, Orientation.volumeForm_comp_linearIsometryEquiv, map_coord_zero, exteriorPower.zeroEquiv_symm_apply, domDomCongr_apply, Module.Basis.is_basis_iff_det, Module.Basis.det_apply, ExteriorAlgebra.liftAlternating_ι, MultilinearMap.alternatization_def, Pi.basisFun_det_apply, Submodule.natAbs_det_basis_change, Orientation.abs_volumeForm_apply_le
instInhabited 📖	CompOp	—
instModule 📖	CompOp	62 math math: Orientation.ne_iff_eq_neg, domLCongr_refl, constLinearEquivOfIsEmpty_symm_apply, constLinearEquivOfIsEmpty_apply, Orientation.volumeForm_neg_orientation, domDomCongrₗ_refl, Orientation.eq_or_eq_neg, ExteriorAlgebra.liftAlternating_ι_mul, ContinuousAlternatingMap.toAlternatingMapLinear_apply, Orientation.map_eq_neg_iff_det_neg, instIsTorsionFree, ContinuousAlternatingMap.toAlternatingMap_curryLeft, Orientation.areaForm_neg_orientation, Orientation.reindex_neg, alternatizeUncurryFin_apply, Orientation.volumeForm_zero_pos, alternatizeUncurryFin_add, curryLeft_apply_apply, Module.Basis.orientation_eq_or_eq_neg, Orientation.kahler_neg_orientation, Orientation.map_eq_det_inv_smul, curryLeft_apply_toMultilinearMap, Module.Basis.orientation_ne_iff_eq_neg, Orientation.rotation_neg_orientation_eq_neg, alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply, domCoprod'_apply, curryLeft_zero, Module.Basis.orientation_comp_linearEquiv_eq_neg_iff_det_neg, ContinuousAlternatingMap.toAlternatingMap_alternatizeUncurryFin, LinearEquiv.alternatingMapCongrRight_apply_apply, curryLeftLinearMap_apply, curryLeft_smul, domDomCongrₗ_toAddEquiv, Orientation.map_neg, uncurryFin_smul, Module.Basis.map_orientation_eq_det_inv_smul, Orientation.rightAngleRotation_trans_neg_orientation, curryLeft_compAlternatingMap, Orientation.volumeForm_zero_neg, uncurryFin_add, Module.Basis.orientation_unitsSMul, Orientation.reindex_apply, curryLeft_compLinearMap, domDomCongrₗ_symm_apply, Orientation.map_apply, uncurryFin_apply, domLCongr_trans, domLCongr_apply, Module.Basis.orientation_neg_single, ExteriorAlgebra.ιMulti_succ_curryLeft, domDomCongrₗ_apply, alternatizeUncurryFin_smul, LinearEquiv.alternatingMapCongrRight_symm_apply_apply, Orientation.eq_or_eq_neg_of_isEmpty, Orientation.oangle_neg_orientation_eq_neg, alternatizeUncurryFinLM_apply, domLCongr_symm, LinearMap.compAlternatingMapₗ_apply, Orientation.rightAngleRotation_neg_orientation, toMultilinearMapLM_apply, curryLeft_add, curryLeft_same
instNeg 📖	CompOp	8 math math: Orientation.volumeForm_robust_neg, Orientation.volumeForm_neg_orientation, OrthonormalBasis.det_eq_neg_det_of_opposite_orientation, Module.Basis.det_adjustToOrientation, neg_apply, OrthonormalBasis.det_adjustToOrientation, coe_neg, Orientation.volumeForm_zero_neg
instSMul 📖	CompOp	14 math math: smul_apply, coe_smul, domDomCongr_smul, Module.Basis.det_unitsSMul, ContinuousAlternatingMap.toAlternatingMap_smul, eq_smul_basis_det, curryLeft_smul, LinearMap.smul_compAlternatingMap, uncurryFin_smul, coeFn_smul, instSMulCommClass, alternatizeUncurryFin_smul, instIsCentralScalar, LinearMap.compAlternatingMap_smul
instSub 📖	CompOp	2 math math: sub_apply, coe_sub
instZero 📖	CompOp	18 math math: domDomCongr_zero, domDomCongr_eq_zero_iff, map_basis_eq_zero_iff, zero_compLinearMap, zero_apply, coe_zero, curryLeft_zero, compLinearMap_zero, ContinuousAlternatingMap.toAlternatingMap_zero, LinearMap.zero_compAlternatingMap, LinearMap.compAlternatingMap_zero, uncurryFin_uncurryFinLM_comp_of_symmetric, Orientation.reindex_apply, Orientation.map_apply, mk_zero, alternatizeUncurryFin_alternatizeUncurryFinLM_comp_of_symmetric, compLinearEquiv_eq_zero_iff, curryLeft_same
ofSubsingleton 📖	CompOp	3 math math: ofSubsingleton_apply_apply, ofSubsingleton_symm_apply_apply, ContinuousAlternatingMap.ofSubsingleton_toAlternatingMap
pi 📖	CompOp	2 math math: coe_pi, pi_apply
prod 📖	CompOp	2 math math: coe_prod, prod_apply
smulRight 📖	CompOp	3 math math: smulRight_apply, LinearMap.smulRight_eq_comp, coe_smulRight
toMultilinearMap 📖	CompOp	23 math math: domCoprod.summand_mk'', coe_pi, coe_prod, domCoprod_coe, coe_smul, map_eq_zero_of_eq', coe_zero, MultilinearMap.domCoprod_alternization_coe, MultilinearMap.domCoprod_alternization_eq, curryLeft_apply_toMultilinearMap, coe_domDomCongr, coe_alternatization, coe_multilinearMap_injective, coe_neg, coe_multilinearMap, toFun_eq_coe, MultilinearMap.alternatization_coe, coe_add, Module.Basis.det_smul_mk_coord_eq_det_update, coe_multilinearMap_mk, coe_sub, toMultilinearMapLM_apply, coe_smulRight
toMultilinearMapLM 📖	CompOp	1 math math: toMultilinearMapLM_apply
uniqueOfCommRing 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
add_compLinearMap 📖	mathematical	—	compLinearMap AlternatingMap instAdd	—	ext
codRestrict_apply_coe 📖	mathematical	Submodule SetLike.instMembership Submodule.setLike DFunLike.coe AlternatingMap instFunLike	Submodule.addCommMonoid Submodule.module codRestrict	—	—
coeFn_smul 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike instSMul Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—
coe_add 📖	mathematical	—	toMultilinearMap AlternatingMap instAdd MultilinearMap MultilinearMap.instAdd	—	—
coe_alternatization 📖	mathematical	—	DFunLike.coe AddMonoidHom MultilinearMap AddCommGroup.toAddCommMonoid AlternatingMap AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup MultilinearMap.instAddCommGroup instAddCommGroup AddMonoidHom.instFunLike MultilinearMap.alternatization toMultilinearMap AddMonoid.toNatSMul Nat.factorial Fintype.card	—	coe_injective Finset.sum_congr domDomCongr_perm Units.smulCommClass_right AddGroup.int_smulCommClass' smul_smul Int.units_mul_self one_smul Finset.sum_const Fintype.card_perm
coe_compLinearMap 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike compLinearMap LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	—
coe_domDomCongr 📖	mathematical	—	toMultilinearMap domDomCongr MultilinearMap.domDomCongr	—	MultilinearMap.ext
coe_inj 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike	—	coe_injective
coe_injective 📖	mathematical	—	AlternatingMap DFunLike.coe instFunLike	—	DFunLike.coe_injective
coe_mk 📖	mathematical	MultilinearMap.toFun AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	DFunLike.coe AlternatingMap instFunLike MultilinearMap MultilinearMap.instFunLikeForall	—	—
coe_multilinearMap 📖	mathematical	—	DFunLike.coe MultilinearMap MultilinearMap.instFunLikeForall toMultilinearMap AlternatingMap instFunLike	—	—
coe_multilinearMap_injective 📖	mathematical	—	AlternatingMap MultilinearMap toMultilinearMap	—	ext MultilinearMap.congr_fun
coe_multilinearMap_mk 📖	mathematical	Function.update AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction MultilinearMap.toFun	toMultilinearMap	—	—
coe_neg 📖	mathematical	—	toMultilinearMap AddCommGroup.toAddCommMonoid AlternatingMap instNeg MultilinearMap MultilinearMap.instNeg	—	—
coe_pi 📖	mathematical	—	toMultilinearMap Pi.addCommMonoid Pi.module pi MultilinearMap.pi	—	—
coe_prod 📖	mathematical	—	toMultilinearMap Prod.instAddCommMonoid Prod.instModule prod MultilinearMap.prod	—	—
coe_smul 📖	mathematical	—	toMultilinearMap AlternatingMap instSMul MultilinearMap MultilinearMap.instSMul DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid	—	—
coe_smulRight 📖	mathematical	—	toMultilinearMap CommSemiring.toSemiring smulRight MultilinearMap.smulRight NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	—
coe_sub 📖	mathematical	—	toMultilinearMap AddCommGroup.toAddCommMonoid AlternatingMap instSub MultilinearMap MultilinearMap.instSub	—	—
coe_zero 📖	mathematical	—	toMultilinearMap AlternatingMap instZero MultilinearMap MultilinearMap.instZero	—	—
compLinearEquiv_eq_zero_iff 📖	mathematical	—	compLinearMap LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AlternatingMap instZero	—	RingHomInvPair.ids LinearEquiv.map_eq_zero_iff AddMonoid.nat_smulCommClass'
compLinearMap_apply 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike compLinearMap LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	—
compLinearMap_assoc 📖	mathematical	—	compLinearMap LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	—
compLinearMap_id 📖	mathematical	—	compLinearMap LinearMap.id	—	ext
compLinearMap_inj 📖	mathematical	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	compLinearMap	—	compLinearMap_injective
compLinearMap_injective 📖	mathematical	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	AlternatingMap compLinearMap	—	ext Function.surjInv_eq ext_iff
compLinearMap_zero 📖	mathematical	—	compLinearMap LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instZero AlternatingMap instZero	—	ext map_zero
congr_arg 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike	—	—
congr_fun 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike	—	—
constLinearEquivOfIsEmpty_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AlternatingMap instAddCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike constLinearEquivOfIsEmpty constOfIsEmpty	—	RingHomInvPair.ids smulCommClass_self
constLinearEquivOfIsEmpty_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AlternatingMap instAddCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm constLinearEquivOfIsEmpty instFunLike Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	RingHomInvPair.ids smulCommClass_self
constOfIsEmpty_apply 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike constOfIsEmpty	—	—
domDomCongrEquiv_apply 📖	mathematical	—	DFunLike.coe AddEquiv AlternatingMap instAdd EquivLike.toFunLike AddEquiv.instEquivLike domDomCongrEquiv domDomCongr	—	—
domDomCongrEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv AlternatingMap instAdd EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm domDomCongrEquiv domDomCongr Equiv.symm	—	—
domDomCongr_add 📖	mathematical	—	domDomCongr AlternatingMap instAdd	—	—
domDomCongr_apply 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike domDomCongr Equiv EquivLike.toFunLike Equiv.instEquivLike	—	—
domDomCongr_eq_iff 📖	mathematical	—	domDomCongr	—	AddEquiv.apply_eq_iff_eq
domDomCongr_eq_zero_iff 📖	mathematical	—	domDomCongr AlternatingMap instZero	—	AddEquiv.map_eq_zero_iff
domDomCongr_perm 📖	mathematical	—	domDomCongr AddCommGroup.toAddCommMonoid Units Int.instMonoid AlternatingMap Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup DFunLike.coe MonoidHom Equiv.Perm MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup Units.instMulOneClass MonoidHom.instFunLike Equiv.Perm.sign	—	ext map_perm
domDomCongr_refl 📖	mathematical	—	domDomCongr Equiv.refl	—	—
domDomCongr_smul 📖	mathematical	—	domDomCongr AlternatingMap instSMul	—	—
domDomCongr_trans 📖	mathematical	—	domDomCongr Equiv.trans	—	—
domDomCongr_zero 📖	mathematical	—	domDomCongr AlternatingMap instZero	—	—
domDomCongrₗ_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AlternatingMap instAddCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike domDomCongrₗ domDomCongr	—	RingHomInvPair.ids
domDomCongrₗ_refl 📖	mathematical	—	domDomCongrₗ Equiv.refl LinearEquiv.refl AlternatingMap instAddCommMonoid instModule	—	RingHomInvPair.ids
domDomCongrₗ_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AlternatingMap instAddCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm domDomCongrₗ domDomCongr Equiv.symm	—	RingHomInvPair.ids
domDomCongrₗ_toAddEquiv 📖	mathematical	—	AddEquivClass.toAddEquiv LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AlternatingMap instAddCommMonoid instModule DFinsupp.instEquivLikeLinearEquiv instAdd SemilinearEquivClass.toAddEquivClass LinearEquiv.instSemilinearEquivClass domDomCongrₗ domDomCongrEquiv	—	RingHomInvPair.ids SemilinearEquivClass.toAddEquivClass LinearEquiv.instSemilinearEquivClass
domLCongr_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AlternatingMap instAddCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike domLCongr compLinearMap LinearEquiv.toLinearMap LinearEquiv.symm	—	RingHomInvPair.ids
domLCongr_refl 📖	mathematical	—	domLCongr LinearEquiv.refl AlternatingMap instAddCommMonoid instModule	—	LinearEquiv.ext RingHomInvPair.ids ext
domLCongr_symm 📖	mathematical	—	LinearEquiv.symm AlternatingMap instAddCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids domLCongr	—	RingHomInvPair.ids
domLCongr_trans 📖	mathematical	—	LinearEquiv.trans AlternatingMap instAddCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids domLCongr	—	RingHomInvPair.ids RingHomCompTriple.ids
ext 📖	—	DFunLike.coe AlternatingMap instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike	—	ext
ext_ring 📖	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule instFunLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	coe_multilinearMap_injective MultilinearMap.ext_ring
ext_ring_iff 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule instFunLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	ext_ring
instIsCentralScalar 📖	mathematical	—	IsCentralScalar AlternatingMap instSMul MulOpposite MulOpposite.instMonoid SMulCommClass.op_right SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	SMulCommClass.op_right ext IsCentralScalar.op_smul_eq_smul
instIsTorsionFree 📖	mathematical	—	Module.IsTorsionFree AlternatingMap instAddCommMonoid instModule	—	Function.Injective.moduleIsTorsionFree Pi.instModuleIsTorsionFree coe_injective coeFn_smul
instSMulCommClass 📖	mathematical	—	SMulCommClass AlternatingMap instSMul	—	ext SMulCommClass.smul_comm
map_add_swap 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup DFunLike.coe AlternatingMap instFunLike Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.swap AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	add_comm map_swap_add
map_congr_perm 📖	mathematical	—	DFunLike.coe AlternatingMap AddCommGroup.toAddCommMonoid instFunLike Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup MonoidHom Equiv.Perm MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup Units.instMulOneClass MonoidHom.instFunLike Equiv.Perm.sign EquivLike.toFunLike Equiv.instEquivLike	—	map_perm smul_smul Int.units_mul_self one_smul
map_coord_zero 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	DFunLike.coe AlternatingMap instFunLike	—	MultilinearMap.map_coord_zero
map_eq_zero_of_eq 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	map_eq_zero_of_eq'
map_eq_zero_of_eq' 📖	mathematical	—	MultilinearMap.toFun toMultilinearMap AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
map_eq_zero_of_not_injective 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Mathlib.Tactic.Push.not_forall_eq Function.Injective.eq_1 map_eq_zero_of_eq
map_linearDependent 📖	mathematical	LinearIndependent Ring.toSemiring AddCommGroup.toAddCommMonoid	DFunLike.coe AlternatingMap instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	not_linearIndependent_iff add_eq_zero_iff_eq_neg Finset.sum_insert Finset.notMem_erase Finset.insert_erase map_update_neg map_update_sum neg_eq_zero Finset.sum_eq_zero Finset.mem_erase map_update_smul map_update_self smul_zero smul_eq_zero IsDomain.toIsCancelMulZero Function.update_eq_self
map_perm 📖	mathematical	—	DFunLike.coe AlternatingMap AddCommGroup.toAddCommMonoid instFunLike Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup Units.instMulOneClass MonoidHom.instFunLike Equiv.Perm.sign	—	Equiv.Perm.swap_induction_on' Finite.of_fintype CompTriple.comp_eq CompTriple.instComp_id CompTriple.instIsIdId Equiv.Perm.sign_one one_smul map_swap Equiv.Perm.sign_mul Equiv.Perm.sign_swap' mul_neg mul_one Units.neg_smul
map_swap 📖	mathematical	—	DFunLike.coe AlternatingMap AddCommGroup.toAddCommMonoid instFunLike Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.swap NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	eq_neg_of_add_eq_zero_left map_swap_add
map_swap_add 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup DFunLike.coe AlternatingMap instFunLike Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.swap AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Equiv.comp_swap_eq_update map_update_add Function.update_comm Function.update_eq_self map_update_self zero_add add_zero map_update_update
map_update_add 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike Function.update AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	MultilinearMap.map_update_add'
map_update_neg 📖	mathematical	—	DFunLike.coe AlternatingMap AddCommGroup.toAddCommMonoid instFunLike Function.update NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	MultilinearMap.map_update_neg
map_update_self 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike Function.update AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	map_eq_zero_of_eq Function.update_self Function.update_of_ne
map_update_smul 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike Function.update SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	MultilinearMap.map_update_smul'
map_update_sub 📖	mathematical	—	DFunLike.coe AlternatingMap AddCommGroup.toAddCommMonoid instFunLike Function.update SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	MultilinearMap.map_update_sub
map_update_sum 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike Function.update Finset.sum	—	MultilinearMap.map_update_sum
map_update_update 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike Function.update AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	map_eq_zero_of_eq Function.update_self Function.update_of_ne
map_update_zero 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike Function.update AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	MultilinearMap.map_update_zero
map_vecCons_add 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike Matrix.vecCons AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	MultilinearMap.cons_add
map_vecCons_smul 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike Matrix.vecCons SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	MultilinearMap.cons_smul
map_zero 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	MultilinearMap.map_zero
mk_zero 📖	mathematical	—	MultilinearMap MultilinearMap.instZero map_eq_zero_of_eq' AlternatingMap instZero	—	map_eq_zero_of_eq'
neg_apply 📖	mathematical	—	DFunLike.coe AlternatingMap AddCommGroup.toAddCommMonoid instFunLike instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
ofSubsingleton_apply_apply 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike Equiv LinearMap RingHom.id Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike ofSubsingleton LinearMap.instFunLike	—	—
ofSubsingleton_symm_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Equiv AlternatingMap EquivLike.toFunLike Equiv.instEquivLike Equiv.symm ofSubsingleton instFunLike	—	—
pi_apply 📖	mathematical	—	DFunLike.coe AlternatingMap Pi.addCommMonoid Pi.module instFunLike pi	—	—
prod_apply 📖	mathematical	—	DFunLike.coe AlternatingMap Prod.instAddCommMonoid Prod.instModule instFunLike prod	—	—
smulRight_apply 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring instFunLike smulRight SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	—
smul_apply 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—
sub_apply 📖	mathematical	—	DFunLike.coe AlternatingMap AddCommGroup.toAddCommMonoid instFunLike instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
toFun_eq_coe 📖	mathematical	—	MultilinearMap.toFun toMultilinearMap DFunLike.coe AlternatingMap instFunLike	—	—
toMultilinearMapLM_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring AlternatingMap MultilinearMap instAddCommMonoid MultilinearMap.addCommMonoid instModule MultilinearMap.instModule LinearMap.instFunLike toMultilinearMapLM toMultilinearMap	—	—
zero_apply 📖	mathematical	—	DFunLike.coe AlternatingMap instFunLike instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
zero_compLinearMap 📖	mathematical	—	compLinearMap AlternatingMap instZero	—	ext

LinearEquiv

Definitions

Name	Category	Theorems
alternatingMapCongrRight 📖	CompOp	2 math math: alternatingMapCongrRight_apply_apply, alternatingMapCongrRight_symm_apply_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
alternatingMapCongrRight_apply_apply 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring AlternatingMap.instFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AlternatingMap.instAddCommMonoid AlternatingMap.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike instEquivLike alternatingMapCongrRight	—	RingHomInvPair.ids smulCommClass_self
alternatingMapCongrRight_symm_apply_apply 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring AlternatingMap.instFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AlternatingMap.instAddCommMonoid AlternatingMap.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike instEquivLike symm alternatingMapCongrRight	—	RingHomInvPair.ids smulCommClass_self

LinearMap

Definitions

Name	Category	Theorems
compAlternatingMap 📖	CompOp	25 math math: coe_compAlternatingMap, compAlternatingMap_apply, exteriorPower.linearMap_ext_iff, ExteriorAlgebra.liftAlternating_comp, ExteriorAlgebra.map_comp_ιMulti, ExteriorAlgebra.liftAlternatingEquiv_symm_apply, compMultilinearMap_alternatization, compAlternatingMap_add, subtype_compAlternatingMap_codRestrict, smulRight_eq_comp, exteriorPower.alternatingMapLinearEquiv_comp_ιMulti, exteriorPower.map_comp_ιMulti, exteriorPower.alternatingMapLinearEquiv_comp, smul_compAlternatingMap, ExteriorAlgebra.liftAlternating_comp_ιMulti, add_compAlternatingMap, zero_compAlternatingMap, AlternatingMap.curryLeft_compAlternatingMap, compAlternatingMap_zero, compAlternatingMap_codRestrict, exteriorPower.alternatingMapLinearEquiv_symm_apply, ExteriorAlgebra.lhom_ext_iff, ExteriorAlgebra.ιMulti_succ_curryLeft, compAlternatingMapₗ_apply, compAlternatingMap_smul
compAlternatingMapₗ 📖	CompOp	1 math math: compAlternatingMapₗ_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_compAlternatingMap 📖	mathematical	—	compAlternatingMap LinearMap RingHom.id Semiring.toNonAssocSemiring instAdd AlternatingMap AlternatingMap.instAdd	—	—
coe_compAlternatingMap 📖	mathematical	—	DFunLike.coe AlternatingMap AlternatingMap.instFunLike compAlternatingMap LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike	—	—
compAlternatingMap_add 📖	mathematical	—	compAlternatingMap AlternatingMap AlternatingMap.instAdd	—	AlternatingMap.ext map_add SemilinearMapClass.toAddHomClass semilinearMapClass
compAlternatingMap_apply 📖	mathematical	—	DFunLike.coe AlternatingMap AlternatingMap.instFunLike compAlternatingMap LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike	—	—
compAlternatingMap_codRestrict 📖	mathematical	Submodule SetLike.instMembership Submodule.setLike DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike	compAlternatingMap Submodule.addCommMonoid Submodule.module codRestrict AlternatingMap.codRestrict AlternatingMap AlternatingMap.instFunLike	—	AlternatingMap.ext
compAlternatingMap_smul 📖	mathematical	—	compAlternatingMap AlternatingMap AlternatingMap.instSMul	—	AlternatingMap.ext map_smul_of_tower
compAlternatingMap_zero 📖	mathematical	—	compAlternatingMap AlternatingMap AlternatingMap.instZero	—	AlternatingMap.ext map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass
compAlternatingMapₗ_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring AlternatingMap AlternatingMap.instAddCommMonoid AlternatingMap.instModule instFunLike compAlternatingMapₗ compAlternatingMap	—	—
compMultilinearMap_alternatization 📖	mathematical	—	DFunLike.coe AddMonoidHom MultilinearMap AddCommGroup.toAddCommMonoid AlternatingMap AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup MultilinearMap.instAddCommGroup AlternatingMap.instAddCommGroup AddMonoidHom.instFunLike MultilinearMap.alternatization compMultilinearMap compAlternatingMap	—	AlternatingMap.ext Finset.sum_congr compMultilinearMap_domDomCongr MultilinearMap.coe_sum Finset.sum_apply map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass map_zsmul_unit
smulRight_eq_comp 📖	mathematical	—	AlternatingMap.smulRight compAlternatingMap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule smulRight IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction id	—	—
smul_compAlternatingMap 📖	mathematical	—	compAlternatingMap LinearMap RingHom.id Semiring.toNonAssocSemiring instSMul DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid AlternatingMap AlternatingMap.instSMul	—	—
subtype_compAlternatingMap_codRestrict 📖	mathematical	Submodule SetLike.instMembership Submodule.setLike DFunLike.coe AlternatingMap AlternatingMap.instFunLike	compAlternatingMap Submodule.addCommMonoid Submodule.module Submodule.subtype AlternatingMap.codRestrict	—	AlternatingMap.ext
zero_compAlternatingMap 📖	mathematical	—	compAlternatingMap LinearMap RingHom.id Semiring.toNonAssocSemiring instZero AlternatingMap AlternatingMap.instZero	—	—

Module.Basis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext_alternating 📖	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring AlternatingMap.instFunLike Module.Basis instFunLike	—	—	AlternatingMap.coe_multilinearMap_injective ext_multilinear Function.Injective.of_comp AlternatingMap.coe_multilinearMap AlternatingMap.map_eq_zero_of_not_injective

MultilinearMap

Definitions

Name	Category	Theorems
alternatization 📖	CompOp	9 math math: LinearMap.compMultilinearMap_alternatization, domCoprod_alternization_coe, domCoprod_alternization_eq, alternatization_apply, AlternatingMap.coe_alternatization, domCoprod_alternization, ContinuousMultilinearMap.alternatization_apply_toAlternatingMap, alternatization_coe, alternatization_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
alternatization_apply 📖	mathematical	—	DFunLike.coe AlternatingMap AddCommGroup.toAddCommMonoid AlternatingMap.instFunLike AddMonoidHom MultilinearMap AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup AlternatingMap.instAddCommGroup AddMonoidHom.instFunLike alternatization Finset.sum Equiv.Perm Finset.univ Equiv.instFintype Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup Units.instMulOneClass MonoidHom.instFunLike Equiv.Perm.sign instFunLikeForall domDomCongr	—	sum_apply Finset.sum_congr
alternatization_coe 📖	mathematical	—	AlternatingMap.toMultilinearMap AddCommGroup.toAddCommMonoid DFunLike.coe AddMonoidHom MultilinearMap AlternatingMap AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup AlternatingMap.instAddCommGroup AddMonoidHom.instFunLike alternatization Finset.sum Equiv.Perm addCommMonoid Finset.univ Equiv.instFintype Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup Units.instMulOneClass MonoidHom.instFunLike Equiv.Perm.sign domDomCongr	—	coe_injective
alternatization_def 📖	mathematical	—	DFunLike.coe AlternatingMap AddCommGroup.toAddCommMonoid AlternatingMap.instFunLike AddMonoidHom MultilinearMap AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup AlternatingMap.instAddCommGroup AddMonoidHom.instFunLike alternatization instFunLikeForall Finset.sum Equiv.Perm addCommMonoid Finset.univ Equiv.instFintype Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup Units.instMulOneClass MonoidHom.instFunLike Equiv.Perm.sign domDomCongr	—	—

(root)

Definitions

Name	Category	Theorems
AlternatingMap 📖	CompData	253 math math: AlternatingMap.sub_apply, Module.Basis.det_comp_basis, AlternatingMap.add_apply, Orientation.ne_iff_eq_neg, LinearMap.coe_compAlternatingMap, AlternatingMap.domLCongr_refl, LinearMap.compAlternatingMap_apply, AlternatingMap.constLinearEquivOfIsEmpty_symm_apply, AlternatingMap.map_vecCons_smul, AlternatingMap.map_perm, AlternatingMap.constLinearEquivOfIsEmpty_apply, AlternatingMap.map_linearDependent, Orientation.volumeForm_robust_neg, AlternatingMap.congr_fun, AlternatingMap.domDomCongr_zero, AlternatingMap.domDomCongr_eq_zero_iff, Orientation.volumeForm_neg_orientation, AlternatingMap.domDomCongrₗ_refl, ExteriorAlgebra.ιMulti_span_fixedDegree, AlternatingMap.smulRight_apply, OrthonormalBasis.det_to_matrix_orthonormalBasis_of_same_orientation, Module.Basis.isUnit_det, OrthonormalBasis.det_eq_neg_det_of_opposite_orientation, OrthonormalBasis.det_to_matrix_orthonormalBasis_of_opposite_orientation, Orientation.eq_or_eq_neg, AlternatingMap.uncurryFin_curryLeft, ExteriorAlgebra.liftAlternating_ι_mul, AlternatingMap.map_update_smul, ContinuousAlternatingMap.toAlternatingMapLinear_apply, exteriorPower.alternatingMapLinearEquiv_ιMulti, AlternatingMap.congr_arg, AlternatingMap.smul_apply, Orientation.volumeForm_map, Module.Basis.det_adjustToOrientation, AlternatingMap.coe_smul, Orientation.map_eq_neg_iff_det_neg, ContinuousAlternatingMap.toAlternatingMap_injective, ExteriorAlgebra.liftAlternating_comp, AlternatingMap.neg_apply, Module.Basis.det_isUnitSMul, Orientation.abs_volumeForm_apply_of_orthonormal, AlternatingMap.instIsTorsionFree, exteriorPower.ιMulti_span_of_span, ContinuousAlternatingMap.toAlternatingMap_curryLeft, AlternatingMap.map_basis_eq_zero_iff, exteriorPower.alternatingMapLinearEquiv_symm_map, AlternatingMap.zero_compLinearMap, ExteriorAlgebra.ιMulti_succ_apply, AlternatingMap.ext_ring_iff, ExteriorAlgebra.ιMulti_span, Orientation.areaForm_to_volumeForm, Orientation.areaForm_neg_orientation, Orientation.reindex_neg, ExteriorAlgebra.ιMulti_zero_apply, AddSubgroup.index_eq_natAbs_det, AlternatingMap.alternatizeUncurryFin_apply, ExteriorAlgebra.liftAlternatingEquiv_symm_apply, LinearMap.compMultilinearMap_alternatization, AlternatingMap.zero_apply, Orientation.volumeForm_zero_pos, AlternatingMap.alternatizeUncurryFin_add, Module.Basis.orientation_eq_iff_det_pos, ZSpan.measureReal_fundamentalDomain, AlternatingMap.map_congr_perm, ExteriorAlgebra.liftAlternating_ιMulti, AlternatingMap.map_update_add, ExteriorAlgebra.liftAlternatingEquiv_apply, LinearMap.compAlternatingMap_add, AlternatingMap.curryLeft_apply_apply, AlternatingMap.domDomCongr_smul, exteriorPower.presentation.relationsSolutionEquiv_symm_apply_var, NumberField.det_basisOfFractionalIdeal_eq_absNorm, ZSpan.measure_fundamentalDomain, AlternatingMap.coe_zero, Module.Basis.det_unitsSMul, Module.Basis.smul_det, MultilinearMap.domCoprod_alternization_coe, AlternatingMap.constOfIsEmpty_apply, ExteriorAlgebra.ιMulti_range, exteriorPower.presentation.relationsSolutionEquiv_apply_apply, Orientation.abs_volumeForm_apply_of_pairwise_orthogonal, ContinuousAlternatingMap.toAlternatingMap_smul, ExteriorAlgebra.liftAlternating_apply_ιMulti, exteriorPower.ιMulti_span_fixedDegree_of_span_eq_top, AlternatingMap.neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq, AlternatingMap.map_update_zero, Module.Basis.orientation_eq_or_eq_neg, exteriorPower.ιMulti_apply_coe, Module.Basis.det_reindex_symm, AlternatingMap.ofSubsingleton_apply_apply, MultilinearMap.domCoprod_alternization_eq, Orientation.kahler_neg_orientation, AlternatingMap.map_eq_zero_of_not_injective, Orientation.map_eq_det_inv_smul, AlternatingMap.coe_mk, AlternatingMap.curryLeft_apply_toMultilinearMap, Module.Basis.orientation_ne_iff_eq_neg, MeasureTheory.Measure.addHaar_parallelepiped, Orientation.rotation_neg_orientation_eq_neg, AlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply, ExteriorAlgebra.liftAlternating_one, AlternatingMap.map_update_sum, AlternatingMap.alternatizeUncurryFin_curryLeft, AlternatingMap.coe_inj, AlternatingMap.map_update_update, AddSubgroup.relIndex_eq_abs_det, AlternatingMap.domCoprod'_apply, AlternatingMap.compLinearMap_injective, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, exteriorPower.alternatingMapLinearEquiv_apply_ιMulti, OrthonormalBasis.det_to_matrix_orthonormalBasis, exteriorPower.ιMultiDual_apply_ιMulti, AlternatingMap.curryLeft_zero, exteriorPower.pairingDual_ιMulti_ιMulti, exteriorPower.alternatingMapLinearEquiv_comp_ιMulti, Module.Basis.det_reindex, exteriorPower.oneEquiv_symm_apply, Module.Basis.orientation_comp_linearEquiv_eq_neg_iff_det_neg, AlternatingMap.map_eq_zero_of_eq, ContinuousAlternatingMap.toAlternatingMap_alternatizeUncurryFin, InnerProductSpace.gramSchmidtOrthonormalBasis_det, AlternatingMap.eq_smul_basis_det, OrthonormalBasis.det_adjustToOrientation, AlternatingMap.coe_injective, AlternatingMap.domDomCongrEquiv_apply, LinearEquiv.alternatingMapCongrRight_apply_apply, exteriorPower.pairingDual_apply_apply_eq_one, ZLattice.covolume_eq_det_mul_measureReal, AlternatingMap.compLinearMap_zero, ContinuousAlternatingMap.toAlternatingMap_zero, AlternatingMap.curryLeftLinearMap_apply, AlternatingMap.map_update_neg, Module.Basis.det_comp, MultilinearMap.alternatization_apply, AlternatingMap.map_vecCons_add, ExteriorAlgebra.ιMulti_apply, exteriorPower.alternatingMapLinearEquiv_comp, AlternatingMap.curryLeft_smul, AlternatingMap.domDomCongr_add, AlternatingMap.domDomCongrₗ_toAddEquiv, AlternatingMap.coe_alternatization, ContinuousAlternatingMap.range_toAlternatingMap, Orientation.map_neg, exteriorPower.alternatingMapToDual_apply_ιMulti, Module.Basis.abs_det_adjustToOrientation, Module.Basis.det_self, AlternatingMap.coe_multilinearMap_injective, LinearMap.smul_compAlternatingMap, Module.Basis.det_basis, AlternatingMap.map_update_sub, Module.Basis.det_inv, AlternatingMap.uncurryFin_smul, MultilinearMap.domCoprod_alternization, exteriorPower.zeroEquiv_ιMulti, ExteriorAlgebra.liftAlternating_comp_ιMulti, AlternatingMap.coe_neg, AlternatingMap.prod_apply, Module.Basis.map_orientation_eq_det_inv_smul, AlternatingMap.coeFn_smul, Orientation.rightAngleRotation_trans_neg_orientation, Orientation.volumeForm_robust', AlternatingMap.ext_iff, AlternatingMap.ofSubsingleton_symm_apply_apply, AlternatingMap.coe_multilinearMap, LinearMap.add_compAlternatingMap, AlternatingMap.map_update_self, LinearMap.zero_compAlternatingMap, AlternatingMap.map_zero, AlternatingMap.toFun_eq_coe, ContinuousMultilinearMap.alternatization_apply_toAlternatingMap, AlternatingMap.curryLeft_compAlternatingMap, Orientation.volumeForm_zero_neg, LinearMap.compAlternatingMap_zero, MultilinearMap.alternatization_coe, ExteriorAlgebra.map_apply_ιMulti, LinearMap.compAlternatingMap_codRestrict, AlternatingMap.measure_def, AlternatingMap.uncurryFin_add, exteriorPower.pairingDual_apply_apply_eq_one_zero, Orientation.volumeForm_apply_le, FractionalIdeal.abs_det_basis_change, Module.Basis.det_mul_det, ExteriorAlgebra.liftAlternating_algebraMap, AlternatingMap.coe_add, AlternatingMap.map_swap, Module.Basis.orientation_unitsSMul, exteriorPower.alternatingMapLinearEquiv_symm_apply, Orientation.reindex_apply, AlternatingMap.measure_parallelepiped, ContinuousAlternatingMap.toAlternatingMap_add, AlternatingMap.coe_compLinearMap, AlternatingMap.curryLeft_compLinearMap, AlternatingMap.domDomCongr_perm, exteriorPower.map_apply_ιMulti, AlternatingMap.map_swap_add, AlternatingMap.domDomCongrₗ_symm_apply, Orientation.map_apply, AlternatingMap.mk_zero, AlternatingMap.uncurryFin_apply, AlternatingMap.map_add_swap, AlternatingMap.compLinearMap_apply, AlternatingMap.instSMulCommClass, AlternatingMap.neg_one_pow_smul_map_insertNth, AlternatingMap.domLCongr_trans, AddSubgroup.relIndex_eq_natAbs_det, AlternatingMap.domLCongr_apply, AlternatingMap.map_insertNth, exteriorPower.presentation_var, Module.Basis.orientation_neg_single, ExteriorAlgebra.ιMulti_succ_curryLeft, Module.Basis.det_unitsSMul_self, AlternatingMap.domDomCongrₗ_apply, Module.Basis.det_smul_mk_coord_eq_det_update, AlternatingMap.pi_apply, AlternatingMap.alternatizeUncurryFin_smul, LinearEquiv.alternatingMapCongrRight_symm_apply_apply, ContinuousAlternatingMap.coe_toAlternatingMap, OrthonormalBasis.det_to_matrix_orthonormalBasis_real, exteriorPower.ιMulti_span_fixedDegree, AlternatingMap.domCoprod_apply, Orientation.eq_or_eq_neg_of_isEmpty, Orientation.oangle_neg_orientation_eq_neg, exteriorPower.oneEquiv_ιMulti, exteriorPower.ιMulti_span, AlternatingMap.coe_sub, exteriorPower.toTensorPower_apply_ιMulti, AlternatingMap.alternatizeUncurryFinLM_apply, Module.Basis.det_map, Ideal.natAbs_det_basis_change, OrthonormalBasis.abs_det_adjustToOrientation, Orientation.volumeForm_comp_linearIsometryEquiv, AlternatingMap.map_coord_zero, ContinuousAlternatingMap.ofSubsingleton_toAlternatingMap, exteriorPower.zeroEquiv_symm_apply, AlternatingMap.domLCongr_symm, AlternatingMap.domDomCongr_apply, LinearMap.compAlternatingMapₗ_apply, Orientation.rightAngleRotation_neg_orientation, Module.Basis.is_basis_iff_det, Module.Basis.det_apply, ExteriorAlgebra.liftAlternating_ι, AlternatingMap.compLinearEquiv_eq_zero_iff, AlternatingMap.toMultilinearMapLM_apply, AlternatingMap.domDomCongrEquiv_symm_apply, AlternatingMap.add_compLinearMap, AlternatingMap.curryLeft_add, AlternatingMap.curryLeft_same, AlternatingMap.instIsCentralScalar, MultilinearMap.alternatization_def, Pi.basisFun_det_apply, LinearMap.compAlternatingMap_smul, Submodule.natAbs_det_basis_change, Orientation.abs_volumeForm_apply_le
«term_[⋀^_]→ₗ[_]_» 📖	CompOp	—

---

← Back to Index