Documentation Verification Report

PowTransition

📁 Source: Mathlib/RingTheory/Ideal/Quotient/PowTransition.lean

Statistics

Metric	Count
Definitions `factorPow`, `factorPowSucc`, `factorPow`, `factorPowSucc`, `powSMulQuotInclusion`	5
Theorems `eq_factor_of_eq_factor_succ`, `factor_ker`, `map_mk_comap_factor`, `map_mk_comap_factorPow`, `eq_factor_of_eq_factor_succ`, `factorPow_comp_powSMulQuotInclusion`, `factor_eq_factor`, `mapQ_eq_factor`, `powSMulQuotInclusion_injective`, `powSMulQuotInclusion_mk`, `pow_smul_top_le`, `range_powSMulQuotInclusion`, `isUnit_of_isUnit_image`	13
Total	18

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_mk_comap_factor` 📖	mathematical	`Ideal` `Ring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`comap` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `instHasQuotient` `RingHom` `Semiring.toNonAssocSemiring` `Quotient.ring` `RingHom.instFunLike` `Quotient.factor` `RingHom.instRingHomClass` `map`	—	`ext` `RingHom.instRingHomClass` `mem_image_of_mem_map_of_surjective` `Quotient.mk_surjective` `Quotient.factor_ker` `map_sub` `RingHomClass.toAddMonoidHomClass` `sub_self` `add_sub_cancel` `map_add` `AddMonoidHomClass.toAddHomClass` `mem_map_of_mem` `Submodule.add_mem`
`map_mk_comap_factorPow` 📖	mathematical	—	`comap` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsScalarTower.right` `Algebra.id` `RingHom` `Semiring.toNonAssocSemiring` `Quotient.ring` `IsTwoSided.instHPowNat` `instIsTwoSided_1` `Quotient.semiring` `RingHom.instFunLike` `Quotient.factorPow` `RingHom.instRingHomClass` `map`	—	`map_mk_comap_factor` `instIsTwoSided_1` `pow_le_self`

Ideal.Quotient

Definitions

Name	Category	Theorems
`factorPow` 📖	CompOp	2 math math: `IsAdicComplete.StrictMono.factorPow_comp_eq_of_factorPow_comp_succ_eq'`, `Ideal.map_mk_comap_factorPow`
`factorPowSucc` 📖	CompOp	2 math math: `WittVector.factorPowSucc_comp_fontaineThetaModPPow`, `WittVector.factorPowSucc_fontaineThetaModPPow_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_factor_of_eq_factor_succ` 📖	mathematical	`Ideal.IsTwoSided` `Ring.toSemiring` `Antitone` `Ideal` `Nat.instPreorder` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal.instHasQuotient` `ring` `RingHom.instFunLike` `factor`	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `Semiring.toNonAssocSemiring` `ring` `RingHom.instFunLike` `factor`	—	`Submodule.eq_factor_of_eq_factor_succ`
`factor_ker` 📖	mathematical	`Ideal` `Ring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`RingHom.ker` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `RingHom` `Semiring.toNonAssocSemiring` `ring` `RingHom.instFunLike` `RingHom.instRingHomClass` `factor` `Ideal.map`	—	`Ideal.ext` `RingHom.instRingHomClass` `mk_surjective` `Ideal.mem_map_of_mem` `Ideal.mem_image_of_mem_map_of_surjective`

Submodule

Definitions

Name	Category	Theorems
`factorPow` 📖	CompOp	3 math math: `IsAdicComplete.StrictMono.factorPow_comp_eq_of_factorPow_comp_succ_eq`, `factorPow_comp_powSMulQuotInclusion`, `IsAdicComplete.StrictMono.factorPow_comp_extend`
`factorPowSucc` 📖	CompOp	—
`powSMulQuotInclusion` 📖	CompOp	5 math math: `range_powSMulQuotInclusion`, `powSMulQuotInclusion_mk`, `factorPow_comp_powSMulQuotInclusion`, `powSMulQuotInclusion_injective`, `AdicCompletion.ofPowSMul_val_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_factor_of_eq_factor_succ` 📖	mathematical	`Antitone` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Nat.instPreorder` `PartialOrder.toPreorder` `instPartialOrder` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `HasQuotient.Quotient` `hasQuotient` `Quotient.addCommGroup` `Quotient.module` `LinearMap.instFunLike` `factor`	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `HasQuotient.Quotient` `Submodule` `AddCommGroup.toAddCommMonoid` `hasQuotient` `Quotient.addCommGroup` `Quotient.module` `LinearMap.instFunLike` `factor`	—	`mapQ_id` `add_tsub_cancel_left` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `LE.le.trans` `factor_comp_apply` `add_assoc`
`factorPow_comp_powSMulQuotInclusion` 📖	mathematical	—	`LinearMap.comp` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `Ideal` `instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `instPowNat` `IsScalarTower.right` `Algebra.id` `Top.top` `instTop` `addCommMonoid` `module` `hasQuotient` `CommRing.toRing` `addCommGroup` `isScalarTower'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `DistribMulAction.toDistribSMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Ring.toSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Quotient.addCommGroup` `Quotient.module` `RingHom.id` `RingHomCompTriple.ids` `factorPow` `powSMulQuotInclusion`	—	`linearMap_qext` `IsScalarTower.left` `IsScalarTower.right` `isScalarTower'` `RingHomCompTriple.ids` `LinearMap.ext`
`factor_eq_factor` 📖	mathematical	`Ideal` `Ring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `HasQuotient.Quotient` `Submodule` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `Semiring.toModule` `hasQuotient` `Quotient.addCommGroup` `Quotient.module` `LinearMap.instFunLike` `factor` `RingHom` `Ideal` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `RingHom.instFunLike` `Ideal.Quotient.factor`	—	—
`mapQ_eq_factor` 📖	mathematical	`Ideal` `Ring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `HasQuotient.Quotient` `Submodule` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `Semiring.toModule` `hasQuotient` `Quotient.addCommGroup` `Quotient.module` `LinearMap.instFunLike` `mapQ` `LinearMap.id` `factor`	—	—
`powSMulQuotInclusion_injective` 📖	mathematical	—	`HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `Ideal` `instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `instPowNat` `IsScalarTower.right` `Algebra.id` `addCommMonoid` `module` `hasQuotient` `CommRing.toRing` `addCommGroup` `isScalarTower'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `DistribMulAction.toDistribSMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Top.top` `instTop` `DFunLike.coe` `LinearMap` `RingHom.id` `Quotient.addCommGroup` `Quotient.module` `LinearMap.instFunLike` `powSMulQuotInclusion`	—	`IsScalarTower.left` `IsScalarTower.right` `isScalarTower'` `LinearMap.ker_eq_bot` `RingHomSurjective.ids` `ker_liftQ` `map.congr_simp` `ker_mkQ` `pow_add` `SemigroupAction.mul_smul` `map_le_map_iff_of_injective` `subtype_injective` `map_comap_subtype` `map_smul''` `map_top` `range_subtype`
`powSMulQuotInclusion_mk` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `HasQuotient.Quotient` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `Ideal` `instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `instPowNat` `IsScalarTower.right` `Algebra.id` `addCommMonoid` `module` `hasQuotient` `CommRing.toRing` `addCommGroup` `isScalarTower'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `DistribMulAction.toDistribSMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Top.top` `instTop` `Quotient.addCommGroup` `Quotient.module` `LinearMap.instFunLike` `powSMulQuotInclusion`	—	`IsScalarTower.left` `IsScalarTower.right` `isScalarTower'`
`pow_smul_top_le` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Ideal` `instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `instPowNat` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Top.top` `instTop`	—	`smul_mono_left` `IsScalarTower.left` `Ideal.pow_le_pow_right`
`range_powSMulQuotInclusion` 📖	mathematical	—	`LinearMap.range` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `Ideal` `instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `instPowNat` `IsScalarTower.right` `Algebra.id` `addCommMonoid` `module` `hasQuotient` `CommRing.toRing` `addCommGroup` `isScalarTower'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `DistribMulAction.toDistribSMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Top.top` `instTop` `Quotient.addCommGroup` `Quotient.module` `RingHom.id` `RingHomSurjective.ids` `powSMulQuotInclusion` `map` `Ring.toSemiring` `mkQ`	—	`IsScalarTower.left` `IsScalarTower.right` `isScalarTower'` `RingHomSurjective.ids` `range_liftQ` `LinearMap.range_comp` `map.congr_simp` `range_subtype` `map_smul''`

factorPowSucc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isUnit_of_isUnit_image` 📖	mathematical	`IsUnit` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Ideal.Quotient.semiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `Ideal.Quotient.factorPow`	`IsUnit` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ideal.Quotient.semiring`	—	`IsScalarTower.right` `IsScalarTower.left` `Ideal.IsTwoSided.instHPowNat` `Ideal.instIsTwoSided_1` `isUnit_iff_exists` `Ideal.pow_le_pow_right` `Ideal.Quotient.factor_surjective` `Ideal.mem_image_of_mem_map_of_surjective` `RingHom.instRingHomClass` `Ideal.Quotient.mk_surjective` `Ideal.Quotient.factor_ker` `RingHom.sub_mem_ker_iff` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `IsUnit.of_mul_eq_one` `instIsDedekindFiniteMonoid` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `mul_sub` `mul_one` `sub_add_sub_cancel'` `sub_eq_self` `Ideal.Quotient.eq_zero_iff_mem` `pow_add` `Ideal.mul_mem_mul` `Ideal.mul_le_left`

---

← Back to Index