Documentation Verification Report

Pointwise

📁 Source: Mathlib/RingTheory/Ideal/Pointwise.lean

Statistics

Metric	Count
Definitions `pointwiseDistribMulAction`, `pointwiseMulSemiringAction`	2
Theorems `smul`, `smul_iff`, `inertia_le_stabilizer`, `instCovariantClassHSMulLe`, `instNormalSubtypeMemSubgroupStabilizerSubgroupOfInertia`, `mem_inv_pointwise_smul_iff`, `mem_pointwise_smul_iff_inv_smul_mem`, `pointwise_central_scalar`, `pointwise_smul_def`, `pointwise_smul_eq_comap`, `pointwise_smul_le_pointwise_smul_iff`, `pointwise_smul_subset_iff`, `pointwise_smul_toAddSubgroup`, `pointwise_smul_toAddSubmonoid`, `smul_bot`, `smul_closure`, `smul_mem_pointwise_smul`, `smul_mem_pointwise_smul_iff`, `smul_sup`, `subset_pointwise_smul_iff`	20
Total	22

Ideal

Definitions

Name	Category	Theorems
`pointwiseDistribMulAction` 📖	CompOp	40 math math: `Quotient.map_ker_stabilizer_subtype`, `relNorm_smul`, `smul_closure`, `mem_pointwise_smul_iff_inv_smul_mem`, `exists_smul_eq_of_isGaloisGroup`, `subset_pointwise_smul_iff`, `LiesOver.smul`, `smul_sup`, `Quotient.stabilizerHom_surjective`, `pointwise_smul_subset_iff`, `instCovariantClassHSMulLe`, `Algebra.IsInvariant.exists_smul_of_under_eq`, `under_smul`, `card_stabilizer_eq`, `IsPrime.smul_iff`, `Quotient.stabilizerHom_surjective_of_profinite`, `inertia_le_stabilizer`, `Algebra.IsInvariant.orbit_eq_primesOver`, `IsFractionRing.stabilizerHom_surjective`, `Quotient.stabilizerHom_apply`, `Algebra.IsInvariant.exists_smul_of_under_eq_of_profinite`, `Quotient.stabilizerQuotientInertiaEquiv_mk`, `coe_smul_primesOver_mk`, `pointwise_smul_eq_comap`, `IsPrime.smul`, `smul_mem_pointwise_smul`, `Quotient.ker_stabilizerHom`, `smul_bot`, `pointwise_smul_le_pointwise_smul_iff`, `card_stabilizer_eq_card_inertia_mul_finrank`, `pointwise_central_scalar`, `pointwise_smul_toAddSubgroup`, `smul_mem_pointwise_smul_iff`, `coe_smul_primesOver`, `exists_map_eq_of_isGalois`, `instNormalSubtypeMemSubgroupStabilizerSubgroupOfInertia`, `IsArithFrobAt.conj`, `pointwise_smul_toAddSubmonoid`, `mem_inv_pointwise_smul_iff`, `pointwise_smul_def`
`pointwiseMulSemiringAction` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inertia_le_stabilizer` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `inertia` `DistribMulAction.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `MulSemiringAction.toDistribMulAction` `MulAction.stabilizer` `Ideal` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `pointwiseDistribMulAction`	—	`SetLike.ext` `mem_pointwise_smul_iff_inv_smul_mem` `add_mem_iff_left` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass` `Subgroup.instSubgroupClass` `add_sub_cancel`
`instCovariantClassHSMulLe` 📖	mathematical	—	`CovariantClass` `Ideal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `pointwiseDistribMulAction` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`map_mono`
`instNormalSubtypeMemSubgroupStabilizerSubgroupOfInertia` 📖	mathematical	—	`Subgroup.Normal` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `Ideal` `Ring.toSemiring` `DistribMulAction.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `pointwiseDistribMulAction` `Subgroup.toGroup` `Subgroup.subgroupOf` `inertia` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `MulSemiringAction.toDistribMulAction`	—	`Subgroup.normal_subgroupOf_iff` `inertia_le_stabilizer` `Submodule.mem_toAddSubgroup` `smul_mem_pointwise_smul_iff` `smul_sub` `smul_smul` `mul_assoc` `inv_mul_cancel_left` `SemigroupAction.mul_smul` `Subgroup.inv_mem`
`mem_inv_pointwise_smul_iff` 📖	mathematical	—	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `pointwiseDistribMulAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `NonAssocSemiring.toAddCommMonoidWithOne` `MulSemiringAction.toDistribMulAction`	—	`mem_pointwise_smul_iff_inv_smul_mem` `inv_inv`
`mem_pointwise_smul_iff_inv_smul_mem` 📖	mathematical	—	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `pointwiseDistribMulAction` `NonAssocSemiring.toAddCommMonoidWithOne` `MulSemiringAction.toDistribMulAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`inv_smul_smul` `smul_mem_pointwise_smul` `smul_inv_smul`
`pointwise_central_scalar` 📖	mathematical	—	`IsCentralScalar` `Ideal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `pointwiseDistribMulAction` `MulOpposite` `MulOpposite.instMonoid`	—	`RingHom.ext` `IsCentralScalar.op_smul_eq_smul`
`pointwise_smul_def` 📖	mathematical	—	`Ideal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `pointwiseDistribMulAction` `map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `MulSemiringAction.toRingHom`	—	—
`pointwise_smul_eq_comap` 📖	mathematical	—	`Ideal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `pointwiseDistribMulAction` `comap` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `DFunLike.coe` `MonoidHom` `RingAut` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RingAut.instGroup` `MonoidHom.instFunLike` `MulSemiringAction.toRingAut` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`	—	`ext` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `comap_symm`
`pointwise_smul_le_pointwise_smul_iff` 📖	mathematical	—	`Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `pointwiseDistribMulAction`	—	`inv_smul_smul` `smul_mono_right` `instCovariantClassHSMulLe`
`pointwise_smul_subset_iff` 📖	mathematical	—	`Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `pointwiseDistribMulAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`pointwise_smul_le_pointwise_smul_iff` `inv_smul_smul`
`pointwise_smul_toAddSubgroup` 📖	mathematical	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `Ring.toSemiring`	`Submodule.toAddSubgroup` `Ring.toAddCommGroup` `Semiring.toModule` `Ideal` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `pointwiseDistribMulAction` `AddSubgroup` `AddCommGroup.toAddGroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `AddSubgroup.pointwiseMulAction`	—	`AddSubgroup.ext` `mem_map_iff_of_surjective` `RingHom.instRingHomClass`
`pointwise_smul_toAddSubmonoid` 📖	mathematical	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction`	`Submodule.toAddSubmonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Ideal` `Submodule.instAddCommMonoidWithOne` `pointwiseDistribMulAction` `AddSubmonoid` `AddCommMonoid.toAddMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `AddSubmonoid.pointwiseMulAction`	—	`AddSubmonoid.ext` `mem_map_iff_of_surjective` `RingHom.instRingHomClass`
`smul_bot` 📖	mathematical	—	`Ideal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `pointwiseDistribMulAction` `Bot.bot` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`map_bot` `RingHom.instRingHomClass`
`smul_closure` 📖	mathematical	—	`Ideal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `pointwiseDistribMulAction` `span` `Set` `Set.smulSet` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `MulSemiringAction.toDistribMulAction`	—	`map_span` `RingHom.instRingHomClass`
`smul_mem_pointwise_smul` 📖	mathematical	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `pointwiseDistribMulAction` `NonAssocSemiring.toAddCommMonoidWithOne` `MulSemiringAction.toDistribMulAction`	—	`subset_span` `Set.smul_mem_smul_set`
`smul_mem_pointwise_smul_iff` 📖	mathematical	—	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `pointwiseDistribMulAction` `NonAssocSemiring.toAddCommMonoidWithOne` `MulSemiringAction.toDistribMulAction`	—	`inv_smul_smul` `smul_mem_pointwise_smul`
`smul_sup` 📖	mathematical	—	`Ideal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `pointwiseDistribMulAction` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`map_sup` `RingHom.instRingHomClass`
`subset_pointwise_smul_iff` 📖	mathematical	—	`Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `pointwiseDistribMulAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`pointwise_smul_le_pointwise_smul_iff` `inv_smul_smul`

Ideal.IsPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul` 📖	mathematical	—	`Ideal.IsPrime` `Ideal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Ideal.pointwiseDistribMulAction`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `Ideal.pointwise_smul_eq_comap` `comap`
`smul_iff` 📖	mathematical	—	`Ideal.IsPrime` `Ideal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Ideal.pointwiseDistribMulAction`	—	`smul` `inv_smul_smul`

---

← Back to Index