PowTransition

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

Statistics

Metric	Count
Definitions factorPow, factorPowSucc, factorPow, factorPowSucc	4
Theorems eq_factor_of_eq_factor_succ, factor_ker, map_mk_comap_factor, map_mk_comap_factorPow, eq_factor_of_eq_factor_succ, factor_eq_factor, mapQ_eq_factor, pow_smul_top_le, isUnit_of_isUnit_image	9
Total	13

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 instHasQuotient RingHom 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	1 math math: 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 📖	—	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	—	—	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.instHasQuotient RingHom 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	—
factorPowSucc 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_factor_of_eq_factor_succ 📖	—	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	—	—	mapQ_id add_tsub_cancel_left Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid LE.le.trans factor_comp_apply add_assoc
factor_eq_factor 📖	mathematical	Ideal Ring.toSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	DFunLike.coe LinearMap RingHom.id HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Ring.toAddCommGroup hasQuotient Quotient.addCommGroup Quotient.module LinearMap.instFunLike factor RingHom 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 RingHom.id HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Ring.toAddCommGroup hasQuotient Quotient.addCommGroup Quotient.module LinearMap.instFunLike mapQ LinearMap.id factor	—	—
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

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	CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 IsScalarTower.right Algebra.id	—	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