NilpotentKer

📁 Source: Mathlib/RingTheory/Finiteness/NilpotentKer.lean

Statistics

Metric	Count
Definitions	0
Theorems finite_of_surjective_of_ker_le_nilradical	1
Total	1

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_of_surjective_of_ker_le_nilradical 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker AlgHomClass.toRingHomClass AlgHom.algHomClass nilradical Ideal.FG	Finite CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule	—	AlgHomClass.toRingHomClass AlgHom.algHomClass IsScalarTower.right RingHom.instIsTwoSidedKer Finite.of_surjective RingHomSurjective.ids AlgEquiv.surjective pow_zero Ideal.one_eq_top Finite.of_finite Finite.of_fintype Ideal.instIsTwoSided_1 Ideal.pow_le_pow_right Ideal.Quotient.factor_surjective IsScalarTower.left RingHomCompTriple.ids Submodule.fg_of_fg_map_of_fg_inf_ker LinearMap.IsScalarTower.compatibleSMul Ideal.Quotient.isScalarTower Submodule.map_top LinearMap.range_eq_top_of_surjective Finite.fg_top Submodule.Quotient.smulCommClass IsScalarTower.to_smulCommClass' Finite.of_fg Submodule.FG.pow Finite.trans Algebra.to_smulCommClass TensorProduct.isScalarTower_left Finite.base_change LinearMap.ker_comp Submodule.map_le_map_iff_of_injective Submodule.subtype_injective Submodule.map_smul'' Submodule.map_comap_eq Submodule.range_subtype Submodule.ker_mkQ pow_succ' instReflLe Ideal.mul_le_left RingHomInvPair.ids TensorProduct.isScalarTower Submodule.comap_injective_of_surjective Submodule.mkQ_surjective Submodule.comap_map_mkQ inf_of_le_right Submodule.isScalarTower' Submodule.Quotient.isScalarTower LinearMap.range_comp Submodule.map.congr_simp Submodule.restrictScalars.congr_simp LinearEquiv.range Submodule.range_liftQ Submodule.FG.map Ideal.FG.isNilpotent_iff_le_nilradical

---

← Back to Index