Basic

📁 Source: Mathlib/Algebra/Module/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems support_const_smul_of_ne_zero, support_const_smul_subset, support_smul, support_smul_subset_left, support_smul_subset_right, indicator_const_smul, indicator_const_smul_apply, indicator_smul, indicator_smul_apply, indicator_smul_apply_left, indicator_smul_const, indicator_smul_const_apply, indicator_smul_left, smul_indicator_one_apply, neg_smul, invOf_two_smul_add_invOf_two_smul, inv_intCast_smul_comm, inv_intCast_smul_eq, inv_natCast_smul_comm, inv_natCast_smul_eq, map_inv_intCast_smul, map_inv_natCast_smul	22
Total	22

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
support_const_smul_of_ne_zero 📖	mathematical	—	support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid hasSMul SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Set.ext smul_ne_zero_iff_right IsDomain.toIsCancelMulZero
support_const_smul_subset 📖	mathematical	—	Set Set.instHasSubset support hasSMul SMulZeroClass.toSMul	—	support_smul_subset_right
support_smul 📖	mathematical	—	support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Pi.smul' SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instInter MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	Set.ext smul_ne_zero_iff IsDomain.toIsCancelMulZero
support_smul_subset_left 📖	mathematical	—	Set Set.instHasSubset support Pi.smul' SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass	—	Pi.smul_apply' zero_smul
support_smul_subset_right 📖	mathematical	—	Set Set.instHasSubset support Pi.smul' SMulZeroClass.toSMul	—	Pi.smul_apply' smul_zero

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
indicator_const_smul 📖	mathematical	—	indicator SMulZeroClass.toSMul	—	indicator_const_smul_apply
indicator_const_smul_apply 📖	mathematical	—	indicator SMulZeroClass.toSMul	—	indicator_smul_apply
indicator_smul 📖	mathematical	—	indicator SMulZeroClass.toSMul	—	indicator_smul_apply
indicator_smul_apply 📖	mathematical	—	indicator SMulZeroClass.toSMul	—	smul_zero
indicator_smul_apply_left 📖	mathematical	—	indicator SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass	—	zero_smul
indicator_smul_const 📖	mathematical	—	indicator SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass	—	indicator_smul_const_apply
indicator_smul_const_apply 📖	mathematical	—	indicator SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass	—	indicator_smul_apply_left
indicator_smul_left 📖	mathematical	—	indicator SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass	—	indicator_smul_apply_left
smul_indicator_one_apply 📖	mathematical	—	SMulZeroClass.toSMul MulZeroClass.toZero MulZeroOneClass.toMulZeroClass SMulWithZero.toSMulZeroClass MulZeroClass.toSMulWithZero indicator Pi.instOne MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	mul_one

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
neg_smul 📖	mathematical	—	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction AddCommGroup.toAddCommMonoid instNeg NonUnitalNonAssocRing.toHasDistribNeg NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	smul_def val_neg neg_smul

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
invOf_two_smul_add_invOf_two_smul 📖	mathematical	—	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 Invertible.invOf Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Convex.combo_self invOf_two_add_invOf_two
inv_intCast_smul_comm 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing	—	map_inv_intCast_smul AddMonoidHom.instAddMonoidHomClass
inv_intCast_smul_eq 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing	—	map_inv_intCast_smul AddMonoidHom.instAddMonoidHomClass
inv_natCast_smul_comm 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Module.toDistribMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	map_inv_natCast_smul AddMonoidHom.instAddMonoidHomClass
inv_natCast_smul_eq 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Module.toDistribMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	map_inv_natCast_smul AddMonoidHom.instAddMonoidHomClass
map_inv_intCast_smul 📖	mathematical	—	DFunLike.coe SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing	—	Int.cast_natCast map_inv_natCast_smul Int.cast_neg inv_neg neg_smul map_neg
map_inv_natCast_smul 📖	mathematical	—	DFunLike.coe SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Module.toDistribMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	inv_zero zero_smul map_zero AddMonoidHomClass.toZeroHomClass inv_smul_smul₀ map_natCast_smul smul_zero smul_inv_smul₀

---

← Back to Index