StronglyTranscendental

📁 Source: Mathlib/RingTheory/Algebraic/StronglyTranscendental.lean

Statistics

Metric	Count
Definitions IsStronglyTranscendental	1
Theorems iff_of_isFractionRing, iff_of_isLocalization, of_isLocalization, of_isLocalization_left, of_map, of_surjective_left, of_transcendental, restrictScalars, transcendental, isStronglyTranscendental_iff_of_field, isStronglyTranscendental_mk_of_mem_minimalPrimes	11
Total	12

IsStronglyTranscendental

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_of_isFractionRing 📖	mathematical	—	IsStronglyTranscendental Transcendental DivisionRing.toRing Field.toDivisionRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap	—	FaithfulSMul.trans IsScalarTower.right IsFractionRing.instFaithfulSMul iff_of_isLocalization le_rfl isStronglyTranscendental_iff_of_field
iff_of_isLocalization 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Semiring.toMonoidWithZero	IsStronglyTranscendental DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	of_map IsLocalization.injective of_isLocalization
of_isLocalization 📖	mathematical	IsStronglyTranscendental	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	IsLocalization.exists_mk'_eq Polynomial.aeval_algebraMap_apply IsLocalization.smul_mk' Algebra.smul_def map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Polynomial.map_mul Polynomial.map_map Polynomial.map_C Polynomial.map_zero Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.add_pf_zero_add 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_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add IsUnit.mul_right_cancel IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass IsLocalization.map_units mul_assoc mul_comm SemigroupAction.mul_smul IsLocalization.smul_mk'_self MulZeroClass.zero_mul
of_isLocalization_left 📖	—	IsStronglyTranscendental	—	—	IsLocalization.integerNormalization_map_to_map Polynomial.aeval_map_algebraMap AlgHom.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul Polynomial.isScalarTower IsScalarTower.right Algebra.smul_mul_assoc smul_zero IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsLocalization.map_units MulZeroClass.mul_zero Algebra.smul_def Polynomial.map_mul Polynomial.map_C mul_assoc Polynomial.map_map IsScalarTower.algebraMap_eq
of_map 📖	—	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike IsStronglyTranscendental	—	—	Polynomial.aeval_algHom_apply AlgHom.algHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass map_eq_zero_iff RingHom.instRingHomClass Polynomial.map_injective Polynomial.coe_mapRingHom Polynomial.map_mul Polynomial.map_C AlgHom.coe_toRingHom Polynomial.map_map AlgHom.comp_algebraMap
of_surjective_left 📖	—	IsStronglyTranscendental DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	—	Polynomial.map_surjective Polynomial.map_map Polynomial.aeval_map_algebraMap
of_transcendental 📖	mathematical	Transcendental DivisionRing.toRing Field.toDivisionRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap	IsStronglyTranscendental	—	FaithfulSMul.trans IsScalarTower.right of_map FaithfulSMul.algebraMap_injective isStronglyTranscendental_iff_of_field
restrictScalars 📖	—	IsStronglyTranscendental	—	—	Polynomial.map_map Polynomial.aeval_map_algebraMap
transcendental 📖	mathematical	IsStronglyTranscendental	Transcendental CommRing.toRing	—	transcendental_iff Polynomial.ext mul_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Polynomial.coeff_map

(root)

Definitions

Name	Category	Theorems
IsStronglyTranscendental 📖	MathDef	7 math math: IsStronglyTranscendental.of_transcendental, isStronglyTranscendental_mk_radical_conductor, isStronglyTranscendental_iff_of_field, Algebra.not_isStronglyTranscendental_of_weaklyQuasiFiniteAt, IsStronglyTranscendental.iff_of_isFractionRing, IsStronglyTranscendental.iff_of_isLocalization, Algebra.not_isStronglyTranscendental_of_quasiFiniteAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isStronglyTranscendental_iff_of_field 📖	mathematical	—	IsStronglyTranscendental EuclideanDomain.toCommRing Field.toEuclideanDomain Transcendental DivisionRing.toRing Field.toDivisionRing	—	IsStronglyTranscendental.transcendental IsDomain.to_noZeroDivisors instIsDomain Polynomial.instNoZeroDivisors Polynomial.coeff_map Polynomial.nontrivial EuclideanDomain.toNontrivial RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
isStronglyTranscendental_mk_of_mem_minimalPrimes 📖	mathematical	IsStronglyTranscendental Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership minimalPrimes	HasQuotient.Quotient Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.commRing Ideal.instAlgebraQuotient DFunLike.coe RingHom Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike	—	Ideal.instIsTwoSided_1 Function.Surjective.forall Ideal.Quotient.mk_surjective Ring.KrullDimLE.of_isLocalization Localization.isLocalization Ring.KrullDimLE.isField_of_isReduced instIsReducedLocalization Localization.AtPrime.isLocalRing IsLocalization.map_eq_zero_iff Ideal.mem_bot Field.instIsLocalRing IsLocalRing.maximalIdeal_eq_bot Localization.AtPrime.map_eq_maximalIdeal Ideal.mem_map_of_mem Ideal.Quotient.eq_zero_iff_mem map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Ideal.Quotient.algebraMap_eq Polynomial.aeval_algebraMap_apply Ideal.Quotient.isScalarTower IsScalarTower.right Polynomial.ext Polynomial.coeff_mul_C Polynomial.coeff_map Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.add_pf_zero_add 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_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Ideal.IsPrime.mem_or_mem_of_mul_eq_zero

---

← Back to Index