📁 Source: Mathlib/RingTheory/Finiteness/NilpotentKer.lean
finite_of_surjective_of_ker_le_nilradical
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
NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring
NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing
NonUnitalCommRing.toNonUnitalNonAssocCommRing
CommRing.toNonUnitalCommRing
Algebra.toModule
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'
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