Fin

📁 Source: Mathlib/LinearAlgebra/Alternating/Uncurry/Fin.lean

Statistics

Metric	Count
Definitions alternatizeUncurryFin, alternatizeUncurryFinLM, uncurryFin, uncurryFinLM	4
Theorems alternatizeUncurryFinLM_apply, alternatizeUncurryFin_add, alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply, alternatizeUncurryFin_alternatizeUncurryFinLM_comp_of_symmetric, alternatizeUncurryFin_apply, alternatizeUncurryFin_curryLeft, alternatizeUncurryFin_smul, map_insertNth, neg_one_pow_smul_map_insertNth, neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq, uncurryFin_add, uncurryFin_apply, uncurryFin_curryLeft, uncurryFin_smul, uncurryFin_uncurryFinLM_comp_of_symmetric	15
Total	19

AlternatingMap

Definitions

Name	Category	Theorems
alternatizeUncurryFin 📖	CompOp	13 math math: uncurryFin_curryLeft, alternatizeUncurryFin_apply, alternatizeUncurryFin_add, alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply, alternatizeUncurryFin_curryLeft, ContinuousAlternatingMap.toAlternatingMap_alternatizeUncurryFin, uncurryFin_smul, uncurryFin_add, uncurryFin_uncurryFinLM_comp_of_symmetric, uncurryFin_apply, alternatizeUncurryFin_smul, alternatizeUncurryFinLM_apply, alternatizeUncurryFin_alternatizeUncurryFinLM_comp_of_symmetric
alternatizeUncurryFinLM 📖	CompOp	4 math math: alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply, uncurryFin_uncurryFinLM_comp_of_symmetric, alternatizeUncurryFinLM_apply, alternatizeUncurryFin_alternatizeUncurryFinLM_comp_of_symmetric
uncurryFin 📖	CompOp	—
uncurryFinLM 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
alternatizeUncurryFinLM_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AlternatingMap AddCommGroup.toAddCommMonoid instAddCommMonoid instModule smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.addCommMonoid LinearMap.module instSMulCommClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike alternatizeUncurryFinLM alternatizeUncurryFin	—	smulCommClass_self instSMulCommClass
alternatizeUncurryFin_add 📖	mathematical	—	alternatizeUncurryFin LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AlternatingMap AddCommGroup.toAddCommMonoid instAddCommMonoid instModule smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instAdd instAdd	—	smulCommClass_self ext alternatizeUncurryFin_apply Finset.sum_congr smul_add Finset.sum_add_distrib
alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike alternatizeUncurryFin LinearMap.comp LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid instModule smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.addCommMonoid LinearMap.module instSMulCommClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHomCompTriple.ids alternatizeUncurryFinLM Finset.sum Finset.univ Fin.fintype Finset.Ici PartialOrder.toPreorder Fin.instPartialOrder Fin.instLocallyFiniteOrderTop SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Monoid.toNatPow Int.instMonoid SubNegMonoid.toSub LinearMap.instFunLike Fin.removeNth	—	smulCommClass_self instSMulCommClass RingHomCompTriple.ids alternatizeUncurryFin_apply Finset.sum_congr Finset.smul_sum Fin.sum_sum_eq_sum_triangle_add Fintype.sum_congr Fin.succAbove_of_le_castSucc Finset.mem_Ici Fin.succAbove_of_castSucc_lt pow_add pow_one SemigroupAction.mul_smul neg_one_smul smul_neg SMulCommClass.smul_comm AddGroup.int_smulCommClass smul_sub Fin.removeNth_removeNth_eq_swap
alternatizeUncurryFin_alternatizeUncurryFinLM_comp_of_symmetric 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AlternatingMap AddCommGroup.toAddCommMonoid instAddCommMonoid instModule smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module instSMulCommClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero	alternatizeUncurryFin LinearMap.comp RingHomCompTriple.ids alternatizeUncurryFinLM instZero	—	smulCommClass_self instSMulCommClass ext RingHomCompTriple.ids alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply Finset.sum_congr sub_self smul_zero Finset.sum_const_zero
alternatizeUncurryFin_apply 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike alternatizeUncurryFin Finset.sum Finset.univ Fin.fintype SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Monoid.toNatPow Int.instMonoid LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid instModule smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instFunLike Fin.removeNth	—	smulCommClass_self Finset.sum_congr MultilinearMap.coe_sum Finset.sum_apply
alternatizeUncurryFin_curryLeft 📖	mathematical	—	alternatizeUncurryFin curryLeft CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AlternatingMap CommSemiring.toSemiring AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup	—	ext smulCommClass_self alternatizeUncurryFin_apply Finset.sum_congr Fin.insertNth_removeNth Function.update_eq_self Finset.sum_const Fintype.card_fin
alternatizeUncurryFin_smul 📖	mathematical	—	alternatizeUncurryFin LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AlternatingMap AddCommGroup.toAddCommMonoid instAddCommMonoid instModule smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instSMul DistribMulAction.toDistribSMul instDistribMulAction instSMulCommClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSMul	—	smulCommClass_self ext instSMulCommClass alternatizeUncurryFin_apply Finset.sum_congr SMulCommClass.smul_comm AddGroup.int_smulCommClass Finset.smul_sum
map_insertNth 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike Fin.insertNth SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Monoid.toNatPow Int.instMonoid Matrix.vecCons	—	Fin.cons_comp_cycleRange map_perm Matrix.vecCons.eq_1 Fin.sign_cycleRange
neg_one_pow_smul_map_insertNth 📖	mathematical	—	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Monoid.toNatPow Int.instMonoid DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike Fin.insertNth Matrix.vecCons	—	map_insertNth smul_smul pow_add Even.neg_one_pow one_smul
neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Monoid.toNatPow Int.instMonoid DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring instFunLike Fin.removeNth NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Fin.exists_succAbove_eq Fin.insertNth_self_removeNth Fin.removeNth_removeNth_eq_swap Fin.removeNth.eq_1 Fin.succAbove_succAbove_predAbove map_insertNth neg_one_pow_smul_map_insertNth Fin.insertNth_removeNth Function.update_eq_self_iff smul_smul pow_add Fin.neg_one_pow_succAbove_add_predAbove neg_smul SemigroupAction.mul_smul sq pow_mul pow_mul' neg_one_pow_two one_pow one_smul neg_add_cancel
uncurryFin_add 📖	mathematical	—	alternatizeUncurryFin LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AlternatingMap AddCommGroup.toAddCommMonoid instAddCommMonoid instModule smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instAdd instAdd	—	alternatizeUncurryFin_add
uncurryFin_apply 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike alternatizeUncurryFin Finset.sum Finset.univ Fin.fintype SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Monoid.toNatPow Int.instMonoid LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid instModule smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instFunLike Fin.removeNth	—	alternatizeUncurryFin_apply
uncurryFin_curryLeft 📖	mathematical	—	alternatizeUncurryFin curryLeft CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AlternatingMap CommSemiring.toSemiring AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup	—	alternatizeUncurryFin_curryLeft
uncurryFin_smul 📖	mathematical	—	alternatizeUncurryFin LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AlternatingMap AddCommGroup.toAddCommMonoid instAddCommMonoid instModule smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instSMul DistribMulAction.toDistribSMul instDistribMulAction instSMulCommClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSMul	—	alternatizeUncurryFin_smul
uncurryFin_uncurryFinLM_comp_of_symmetric 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AlternatingMap AddCommGroup.toAddCommMonoid instAddCommMonoid instModule smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module instSMulCommClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero	alternatizeUncurryFin LinearMap.comp RingHomCompTriple.ids alternatizeUncurryFinLM instZero	—	alternatizeUncurryFin_alternatizeUncurryFinLM_comp_of_symmetric

---

← Back to Index