Documentation Verification Report

Basic

📁 Source: Mathlib/Algebra/Ring/Action/Basic.lean

Statistics

Metric	Count
Definitions `MulSemiringAction`, `compHom`, `toDistribMulAction`, `toMulDistribMulAction`, `toRingHom`, `applyMulSemiringAction`	6
Theorems `smul_mul`, `smul_one`, `toRingHom_apply`, `applyFaithfulSMul`, `smul_def`, `toRingHom_injective`	6
Total	12

MulSemiringAction

Definitions

Name	Category	Theorems
`compHom` 📖	CompOp	—
`toDistribMulAction` 📖	CompOp	154 math math: `Ideal.Quotient.map_ker_stabilizer_subtype`, `SkewMonoidAlgebra.coeff_single_one_mul`, `Polynomial.smul_mem_rootSet`, `NumberField.RingOfIntegers.instSMulDistribClass`, `SkewMonoidAlgebra.coeff_single_mul_of_not_exists_mul`, `Ideal.smul_closure`, `SkewMonoidAlgebra.single_algebraMap_eq_algebraMap_mul_of`, `Ideal.mem_pointwise_smul_iff_inv_smul_mem`, `MulSemiringActionHom.instMulSemiringActionSemiHomClassCoeMonoidHom`, `Subsemiring.mem_smul_pointwise_iff_exists`, `RingAut.smul_def`, `IsGaloisGroup.fixingSubgroup_top`, `AlgEquiv.apply_smulCommClass'`, `IsGaloisGroup.fixedPoints_top`, `IsGaloisGroup.mulEquivAlgEquiv_apply_symm_apply`, `Subsemiring.smul_mem_pointwise_smul_iff`, `MulSemiringActionHom.map_smulₛₗ`, `Subring.mem_pointwise_smul_iff_inv_smul_mem`, `IsArithFrobAt.mul_inv_mem_inertia`, `Subalgebra.coe_pointwise_smul`, `MulSemiringActionHom.coe_fn_coe'`, `Subring.mem_pointwise_smul_iff_inv_smul_mem₀`, `toRingEquiv_apply`, `Subsemiring.smul_mem_pointwise_smul`, `SkewPolynomial.φ_iterate_apply`, `Subsemiring.pointwise_smul_toAddSubmonoid`, `instSMulDistribClassSubtypeMemSubalgebraIntegralClosure`, `Subring.pointwise_smul_toAddSubgroup`, `Subring.coe_pointwise_smul`, `IsInvariantSubring.smul_mem`, `FixedPoints.instSMulCommClassSubtypeMemSubfieldSubfield`, `SkewMonoidAlgebra.nonUnitalAlgHom_ext'_iff`, `SkewMonoidAlgebra.coeff_mul_single_of_not_exists_mul`, `IsNilpotent.exp_smul`, `SkewMonoidAlgebra.coeff_mul_right`, `prodXSubSMul.smul`, `IsGaloisGroup.fixedPoints_fixingSubgroup`, `AlgEquiv.smul_def`, `IsGaloisGroup.le_fixedPoints_iff_le_fixingSubgroup`, `spinGroup.conjAct_smul_range_ι`, `toAlgEquiv_symm_apply`, `IsGaloisGroup.fixingSubgroup_le_of_le`, `Subring.mem_inv_pointwise_smul_iff`, `charpoly_eq_prod_smul`, `smul_coeff_charpoly`, `MulSemiringActionHom.map_smul`, `SkewMonoidAlgebra.single_mul_single`, `Ideal.inertia_le_stabilizer`, `Polynomial.smul_mem_rootSet_iff`, `instSMulDistribClassAlgEquiv`, `smul_charpoly`, `IsGaloisGroup.faithful`, `RingHom.applyFaithfulSMul`, `Subring.mem_smul_pointwise_iff_exists`, `IsGaloisGroup.fixingSubgroup_fixedPoints`, `IsGaloisGroup.mulEquivAlgEquiv_apply_apply`, `Polynomial.smul_X`, `Ideal.Quotient.stabilizerHom_apply`, `Polynomial.smul_eq_map`, `Subsemiring.smul_mem_pointwise_smul_iff₀`, `SkewMonoidAlgebra.domCongr_refl`, `IsGaloisGroup.fixedPoints_bot`, `Polynomial.smul_eval_smul`, `Subring.smul_closure`, `IsGaloisGroup.ofDual_intermediateFieldEquivSubgroup_apply`, `Ideal.Quotient.stabilizerQuotientInertiaEquiv_mk`, `Polynomial.aeval_smul`, `SkewMonoidAlgebra.coeff_mul`, `instIsInvariantSubtypeMemSubalgebraSubalgebraSubgroupQuotient`, `Subsemiring.mem_inv_pointwise_smul_iff₀`, `toRingEquiv_symm_apply`, `prodXSubSMul.coeff`, `SkewMonoidAlgebra.coeff_mul_antidiagonal_finsum`, `MulSemiringActionHom.map_one'`, `MulSemiringActionHom.coe_fn_coe`, `pinGroup.conjAct_smul_range_ι`, `smul_mul`, `Subring.smul_mem_pointwise_smul_iff₀`, `Subalgebra.smul_mem_pointwise_smul`, `MulSemiringActionHom.map_mul'`, `SkewMonoidAlgebra.support_mul_single_subset`, `IsInvariantSubring.coe_subtypeHom'`, `charpoly_eq`, `SkewMonoidAlgebra.coeff_mul_single`, `SkewMonoidAlgebra.support_mul`, `stabilizer_isOpen_of_isIntegral`, `MulSemiringActionHom.coe_polynomial`, `FixedPoints.smul_polynomial`, `SkewMonoidAlgebra.coeff_mul_single_one`, `Ideal.smul_mem_pointwise_smul`, `IsGaloisGroup.intermediateField`, `Subsemiring.coe_pointwise_smul`, `IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply`, `Ideal.card_inertia_eq_ramificationIdxIn`, `FixedBy.intermediateField_mem_iff`, `toAlgEquiv_apply`, `RingHom.smul_def`, `integralClosure.coe_smul`, `FixedPoints.linearIndependent_smul_of_linearIndependent`, `Ideal.Quotient.ker_stabilizerHom`, `Subsemiring.mem_pointwise_smul_iff_inv_smul_mem`, `NormedSpace.exp_smul`, `SkewMonoidAlgebra.isScalarTower_self`, `isConjRoot_iff_orbitRel`, `IsGaloisGroup.fixingSubgroup_bot`, `IsGaloisGroup.subgroup`, `smul_one`, `Ideal.card_stabilizer_eq_card_inertia_mul_finrank`, `IsGaloisGroup.intermediateFieldEquivSubgroup_apply`, `SkewMonoidAlgebra.support_single_mul_subset`, `SkewMonoidAlgebra.coeff_mul_antidiagonal_of_finset`, `Polynomial.rootSet.coe_smul`, `toAlgHom_apply`, `SkewMonoidAlgebra.single_eq_algebraMap_mul_of`, `Polynomial.smul_mem_rootSet_iff_of_isUnit`, `AlgEquiv.apply_faithfulSMul`, `RingAut.apply_faithfulSMul`, `SkewMonoidAlgebra.coeff_mul_left`, `instSMulCommClassSubtypeMemSubalgebraIntegralClosure`, `IsGaloisGroup.fixedPoints_le_of_le`, `IsLocalRing.ResidueField.residue_smul`, `SkewMonoidAlgebra.coeff_mul_single_aux`, `Subring.smul_mem_pointwise_smul`, `Ideal.ncard_primesOver_mul_card_inertia_mul_finrank`, `Polynomial.smul_eval`, `FixedPoints.smul`, `FixedPoints.smulCommClass'`, `IsInvariantSubfield.smul_mem`, `Subsemiring.smul_closure`, `Subalgebra.pointwise_smul_toSubmodule`, `IsGaloisGroup.card_fixingSubgroup_eq_finrank`, `SkewMonoidAlgebra.coeff_single_mul_aux`, `IntermediateField.forall_mem_adjoin_smul_eq_self_iff`, `IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup`, `Ideal.smul_mem_pointwise_smul_iff`, `FixedPoints.mem_intermediateField_iff`, `Subring.smul_mem_pointwise_smul_iff`, `smul_inv''`, `Ideal.instNormalSubtypeMemSubgroupStabilizerSubgroupOfInertia`, `Subsemiring.mem_pointwise_smul_iff_inv_smul_mem₀`, `instSMulCommClassQuotientSubgroupSubtypeMemSubalgebraSubalgebra`, `Polynomial.eval_smul'`, `Algebra.forall_mem_adjoin_smul_eq_self_iff`, `IsGaloisGroup.commutes`, `lipschitzGroup.conjAct_smul_range_ι`, `Subring.mem_inv_pointwise_smul_iff₀`, `Subsemiring.mem_inv_pointwise_smul_iff`, `IsGaloisGroup.map_mulEquivAlgEquiv_fixingSubgroup`, `Ideal.mem_inv_pointwise_smul_iff`, `SkewMonoidAlgebra.coeff_single_mul`, `IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply_toDual`, `FixedBy.subfield_mem_iff`, `IsCyclotomicExtension.Rat.galEquivZMod_smul_of_pow_eq`, `AlgEquiv.apply_smulCommClass`
`toMulDistribMulAction` 📖	CompOp	12 math math: `toRingHom_apply`, `NumberField.RingOfIntegers.instSMulDistribClass`, `Normal.minpoly_eq_iff_mem_orbit`, `ValuationSubring.mem_inv_pointwise_smul_iff`, `ValuationSubring.mem_pointwise_smul_iff_inv_smul_mem`, `ValuationSubring.smul_mem_pointwise_smul_iff`, `IsGaloisGroup.mulEquivCongr_apply_smul`, `instSMulDistribClassAlgEquiv`, `ValuationSubring.coe_pointwise_smul`, `ValuationSubring.mem_smul_pointwise_iff_exists`, `IsLocalRing.ResidueField.residue_smul`, `ValuationSubring.smul_mem_pointwise_smul`
`toRingHom` 📖	CompOp	7 math math: `Subring.pointwise_smul_def`, `toRingHom_apply`, `toRingHom_injective`, `SkewPolynomial.φ_def`, `Polynomial.smul_eq_map`, `Subsemiring.pointwise_smul_def`, `Ideal.pointwise_smul_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_mul` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `toDistribMulAction` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	—
`smul_one` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `toDistribMulAction` `AddMonoidWithOne.toOne`	—	—
`toRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `toRingHom` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulDistribMulAction.toMulAction` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `toMulDistribMulAction`	—	—

RingHom

Definitions

Name	Category	Theorems
`applyMulSemiringAction` 📖	CompOp	2 math math: `applyFaithfulSMul`, `smul_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`applyFaithfulSMul` 📖	mathematical	—	`FaithfulSMul` `RingHom` `Semiring.toNonAssocSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instMonoid` `MulSemiringAction.toDistribMulAction` `applyMulSemiringAction`	—	`ext`
`smul_def` 📖	mathematical	—	`RingHom` `Semiring.toNonAssocSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instMonoid` `MulSemiringAction.toDistribMulAction` `applyMulSemiringAction` `DFunLike.coe` `instFunLike`	—	—

(root)

Definitions

Name	Category	Theorems
`MulSemiringAction` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toRingHom_injective` 📖	mathematical	—	`RingHom` `Semiring.toNonAssocSemiring` `MulSemiringAction.toRingHom`	—	`FaithfulSMul.eq_of_smul_eq_smul` `RingHom.ext_iff`

---

← Back to Index