Basic

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

Statistics

Metric	Count
Definitions `instTrans`, `«term_≡_[SMOD_]»`	2
Theorems `add`, `bot`, `comap`, `comm`, `def`, `eval`, `instRefl`, `map`, `mono`, `mul`, `neg`, `nsmul`, `of_toAddSubgroup_le`, `pow`, `prod`, `refl`, `rfl`, `smul`, `sub`, `sub_mem`, `sum`, `top`, `trans`, `zero`, `zsmul`, `sub_smodEq_zero`	26
Total	28

SModEq

Definitions

Name	Category	Theorems
`instTrans` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`SModEq`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`def`
`bot` 📖	mathematical	—	`SModEq` `Bot.bot` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instBot`	—	`def` `Submodule.Quotient.eq` `Submodule.mem_bot` `sub_eq_zero`
`comap` 📖	mathematical	`SModEq` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`Submodule.comap`	—	`Submodule.Quotient.eq` `LinearMap.map_sub`
`comm` 📖	mathematical	—	`SModEq`	—	`symm`
`def` 📖	mathematical	—	`SModEq`	—	—
`eval` 📖	mathematical	`SModEq` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Polynomial.eval`	—	`Polynomial.eval_eq_sum` `Finset.sum_congr` `sum` `mul` `refl` `pow`
`instRefl` 📖	mathematical	—	`SModEq`	—	`refl`
`map` 📖	mathematical	`SModEq`	`Submodule.map` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	—	`RingHomSurjective.ids` `Submodule.Quotient.eq` `Submodule.mem_map_of_mem` `LinearMap.map_sub`
`mono` 📖	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `SModEq`	—	—	`Submodule.Quotient.eq`
`mul` 📖	mathematical	`SModEq` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Ideal.instIsTwoSided_1` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass`
`neg` 📖	mathematical	`SModEq`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`nsmul` 📖	mathematical	`SModEq`	`AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`def` `AddCommMonoid.nat_isScalarTower`
`of_toAddSubgroup_le` 📖	—	`AddSubgroup` `AddCommGroup.toAddGroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `Submodule.toAddSubgroup` `SModEq`	—	—	—
`pow` 📖	mathematical	`SModEq` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Ideal.instIsTwoSided_1` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`prod` 📖	mathematical	`SModEq` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Finset.prod` `CommRing.toCommMonoid`	—	`Finset.cons_induction` `Finset.prod_cons` `Mathlib.Tactic.GCongr.rel_imp_rel` `instIsTransOfTrans` `mul` `Finset.mem_cons_self` `refl` `Finset.mem_cons_of_mem`
`refl` 📖	mathematical	—	`SModEq`	—	—
`rfl` 📖	mathematical	—	`SModEq`	—	`refl`
`smul` 📖	mathematical	`SModEq`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`def` `IsScalarTower.left`
`sub` 📖	mathematical	`SModEq`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`def`
`sub_mem` 📖	mathematical	—	`SModEq` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`def` `Submodule.Quotient.eq`
`sum` 📖	mathematical	`SModEq`	`Finset.sum` `AddCommGroup.toAddCommMonoid`	—	`Finset.cons_induction` `Finset.sum_cons` `Mathlib.Tactic.GCongr.rel_imp_rel` `instIsTransOfTrans` `add` `Finset.mem_cons_self` `refl` `Finset.mem_cons_of_mem`
`top` 📖	mathematical	—	`SModEq` `Top.top` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instTop`	—	`Submodule.Quotient.eq` `Submodule.mem_top`
`trans` 📖	—	`SModEq`	—	—	—
`zero` 📖	mathematical	—	`SModEq` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike`	—	`def` `Submodule.Quotient.eq` `sub_zero`
`zsmul` 📖	mathematical	`SModEq`	`SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`def` `AddCommGroup.intIsScalarTower`

(root)

Definitions

Name	Category	Theorems
`«term_≡_[SMOD_]»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sub_smodEq_zero` 📖	mathematical	—	`SModEq` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`sub_zero`

---

← Back to Index