Pointwise

📁 Source: Mathlib/Algebra/Algebra/Subalgebra/Pointwise.lean

Statistics

Metric	Count
Definitions pointwiseMulAction	1
Theorems coe_pointwise_smul, instCovariantClassHSMulLe, isIdempotentElem_toSubmodule, mul_toSubmodule, mul_toSubmodule_le, pointwise_smul_toSubmodule, pointwise_smul_toSubring, pointwise_smul_toSubsemiring, smul_mem_pointwise_smul	9
Total	10

Subalgebra

Definitions

Name	Category	Theorems
pointwiseMulAction 📖	CompOp	6 math math: coe_pointwise_smul, instCovariantClassHSMulLe, smul_mem_pointwise_smul, pointwise_smul_toSubsemiring, pointwise_smul_toSubmodule, pointwise_smul_toSubring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_pointwise_smul 📖	mathematical	—	SetLike.coe Subalgebra instSetLike SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction Set Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction	—	—
instCovariantClassHSMulLe 📖	mathematical	—	CovariantClass Subalgebra SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	map_mono
isIdempotentElem_toSubmodule 📖	mathematical	—	IsIdempotentElem Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Submodule.mul IsScalarTower.right DFunLike.coe OrderEmbedding Subalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding toSubmodule	—	le_antisymm IsScalarTower.right LE.le.trans_eq mul_toSubmodule_le sup_idem mul_one Submodule.mul_mem_mul OneMemClass.one_mem AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass instSubsemiringClass
mul_toSubmodule 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Submodule.mul IsScalarTower.right DFunLike.coe OrderEmbedding Subalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding toSubmodule SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra	—	le_antisymm IsScalarTower.right mul_toSubmodule_le Algebra.adjoin_induction mul_one Submodule.mul_mem_mul OneMemClass.one_mem AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass instSubsemiringClass one_mul algebraMap_mem instSMulMemClass Submodule.add_mem isIdempotentElem_toSubmodule mul_assoc mul_comm
mul_toSubmodule_le 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.mul IsScalarTower.right DFunLike.coe OrderEmbedding Subalgebra instPartialOrder instFunLikeOrderEmbedding toSubmodule SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra	—	IsScalarTower.right Submodule.mul_le MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubsemiringClass.toSubmonoidClass instSubsemiringClass Algebra.mem_sup_left Algebra.mem_sup_right
pointwise_smul_toSubmodule 📖	mathematical	—	DFunLike.coe OrderEmbedding Subalgebra Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding toSubmodule SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Submodule.pointwiseDistribMulAction MulSemiringAction.toDistribMulAction	—	—
pointwise_smul_toSubring 📖	mathematical	—	toSubring Subalgebra CommRing.toCommSemiring Ring.toSemiring SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction Subring Subring.pointwiseMulAction	—	—
pointwise_smul_toSubsemiring 📖	mathematical	—	toSubsemiring Subalgebra SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction Subsemiring Semiring.toNonAssocSemiring Subsemiring.pointwiseMulAction	—	—
smul_mem_pointwise_smul 📖	mathematical	Subalgebra SetLike.instMembership instSetLike	SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction	—	Set.smul_mem_smul_set

---

← Back to Index