Field

📁 Source: Mathlib/RingTheory/Unramified/Field.lean

Statistics

Metric	Count
Definitions	0
Theorems bijective_of_isAlgClosed_of_isLocalRing, iff_isSeparable, isField_of_isAlgClosed_of_isLocalRing, isReduced_of_field, isSeparable, of_isSeparable, range_eq_top_of_isPurelyInseparable, not_minpoly_sq_dvd	8
Total	8

Algebra.FormallyUnramified

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective_of_isAlgClosed_of_isLocalRing 📖	mathematical	—	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	finite_of_free Module.Free.of_divisionRing isArtinian_of_tower IsScalarTower.right isArtinian_of_fg_of_artinian' DivisionRing.instIsArtinianRing IsLocalRing.jacobson_eq_maximalIdeal bot_ne_top Ideal.instNontrivial IsLocalRing.toNontrivial IsArtinianRing.isNilpotent_jacobson_bot IsAlgClosed.algebraMap_bijective_of_isIntegral Ideal.Quotient.isDomain Ideal.instIsTwoSided_1 Ideal.IsMaximal.isPrime' IsLocalRing.maximalIdeal.isMaximal instIsIntegralQuotientIdeal Algebra.IsAlgebraic.isIntegral Algebra.IsAlgebraic.of_finite EuclideanDomain.toNontrivial Equiv.left_inv Equiv.right_inv MonoidHom.map_mul' RingHom.map_add' AlgHom.commutes' Algebra.to_smulCommClass IsScalarTower.to_smulCommClass RingHomCompTriple.ids Ideal.Quotient.isScalarTower LinearMap.comp_assoc IsScalarTower.to_smulCommClass' SMulCommClass.symm IsScalarTower.left LinearMap.IsScalarTower.compatibleSMul LinearMap.instIsScalarTower smulCommClass_self comp_sec LinearMap.restrictScalars_injective TensorProduct.isScalarTower_left TensorProduct.ext' AlgEquiv.surjective Algebra.smul_def mul_comm AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgEquiv.symm_apply_apply Algebra.algebraMap_eq_smul_one LinearMap.congr_fun Ideal.Quotient.eq_zero_iff_mem map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Ideal.Quotient.algebraMap_eq sub_self IsIdempotentElem.one_sub IsIdempotentElem.eq_1 smul_eq_mul map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass Ideal.mem_bot Ideal.zero_eq_bot Ideal.pow_mem_pow sub_eq_zero IsIdempotentElem.pow_succ_eq pow_succ MulZeroClass.zero_mul Equiv.bijective AlgEquiv.commutes mul_one NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass LinearMap.map_smul_of_tower AlgHomClass.toRingHomClass AlgEquiv.apply_symm_apply
iff_isSeparable 📖	mathematical	—	Algebra.FormallyUnramified EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.IsSeparable DivisionRing.toRing Field.toDivisionRing	—	isSeparable of_isSeparable
isField_of_isAlgClosed_of_isLocalRing 📖	mathematical	—	IsField CommSemiring.toSemiring CommRing.toCommSemiring	—	IsLocalRing.isField_iff_maximalIdeal_eq eq_bot_iff Function.Bijective.surjective bijective_of_isAlgClosed_of_isLocalRing RingHom.map_zero IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass isUnit_iff_ne_zero RingHom.congr_arg
isReduced_of_field 📖	mathematical	—	IsReduced MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	RingHomCompTriple.ids map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Module.Flat.rTensor_preserves_injective_linearMap Module.Flat.of_free Module.Free.of_divisionRing RingHom.injective DivisionRing.isSimpleRing EuclideanDomain.toNontrivial AlgEquiv.injective map_zero MonoidWithZeroHomClass.toZeroHomClass Algebra.to_smulCommClass IsScalarTower.right AlgHomClass.toRingHomClass AlgHom.algHomClass eq_zero_of_localization Ideal.IsMaximal.isPrime' IsNilpotent.map Algebra.EssFiniteType.of_isLocalization Localization.isLocalization of_isLocalization Algebra.EssFiniteType.comp OreLocalization.instIsScalarTower Algebra.EssFiniteType.baseChange comp base_change IsNilpotent.eq_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain isField_of_isAlgClosed_of_isLocalRing AlgebraicClosure.isAlgClosed Localization.AtPrime.isLocalRing
isSeparable 📖	mathematical	—	Algebra.IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	—	finite_of_free Module.Free.of_divisionRing separableClosure.eq_top_iff of_restrictScalars IsScalarTower.left IntermediateField.isScalarTower_mid' Algebra.EssFiniteType.of_comp IntermediateField.ext range_eq_top_of_isPurelyInseparable separableClosure.isPurelyInseparable Algebra.IsAlgebraic.of_finite EuclideanDomain.toNontrivial
of_isSeparable 📖	mathematical	—	Algebra.FormallyUnramified EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Ideal.instIsTwoSided_1 iff_comp_injective AlgHom.ext AlgHom.congr_fun Polynomial.eval_add_of_sq_eq_zero Ideal.pow_mem_pow sub_eq_zero IsUnit.mul_right_eq_zero IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass isUnit_iff_ne_zero Polynomial.Separable.aeval_derivative_ne_zero EuclideanDomain.toNontrivial Algebra.IsSeparable.isSeparable minpoly.aeval add_sub_cancel Polynomial.eval_map_algebraMap Polynomial.aeval_algHom_apply map_zero MonoidWithZeroHomClass.toZeroHomClass Polynomial.derivative_map zero_add
range_eq_top_of_isPurelyInseparable 📖	mathematical	—	RingHom.range DivisionRing.toRing Field.toDivisionRing algebraMap Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Top.top Subring Subring.instTop	—	not_subsingleton_iff_nontrivial rank_zero_iff instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IsScalarTower.to_smulCommClass IsScalarTower.left rank_tensorProduct' commRing_strongRankCondition EuclideanDomain.toNontrivial Module.Free.of_divisionRing mul_eq_zero Cardinal.noZeroDivisors top_le_iff IsPurelyInseparable.pow_mem ringExpChar.expChar expChar_of_injective_ringHom RingHom.injective DivisionRing.isSimpleRing sub_pow_expChar_pow Algebra.TensorProduct.tmul_pow one_pow Algebra.algebraMap_eq_smul_one TensorProduct.smul_tmul TensorProduct.CompatibleSMul.isScalarTower sub_self isReduced_of_field Algebra.to_smulCommClass base_change Algebra.EssFiniteType.baseChange sub_eq_zero IsNilpotent.eq_zero LinearIndependent.linearIndepOn_id Set.subset_univ LinearIndepOn.subset_extend Matrix.range_cons Matrix.range_empty Set.union_empty Set.union_singleton Module.Basis.coe_extend map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingHomInvPair.ids DFunLike.congr_fun DFunLike.congr_arg Module.Basis.tensorProduct_repr_tmul_apply Module.Basis.repr_self Finsupp.single_apply mul_one MulZeroClass.mul_zero NeZero.one LinearIndependent.pair_iff isUnit_iff_ne_zero injective_iff_map_eq_zero' RingHomClass.toAddMonoidHomClass add_zero zero_smul map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Algebra.smul_def eq_neg_iff_add_eq_zero smul_neg neg_smul neg_neg smul_smul IsUnit.val_inv_mul one_smul

Algebra.IsUnramifiedAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
not_minpoly_sq_dvd 📖	mathematical	Ideal.span Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.semiring Set Set.instSingletonSet RingHom.ker CommSemiring.toSemiring Semifield.toCommSemiring RingHom Semiring.toNonAssocSemiring CommRing.toCommSemiring RingHom.instFunLike RingHom.instRingHomClass AlgHom.toRingHom Polynomial.algebraOfAlgebra Algebra.id Polynomial.aeval DFunLike.coe AlgHom AlgHom.funLike	EuclideanDomain.toCommRing Field.toEuclideanDomain semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero minpoly Ideal.ResidueField DivisionRing.toRing Field.toDivisionRing IsLocalRing.ResidueField.field Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid IsLocalRing.ResidueField.algebra OreLocalization.instAlgebra algebraMap	—	RingHom.instRingHomClass Algebra.FiniteType.of_surjective Algebra.FiniteType.instPolynomial Algebra.FiniteType.of_finitePresentation Algebra.FinitePresentation.self Algebra.FormallyUnramified.finite_of_free Algebra.instEssFiniteTypeLocalization Algebra.EssFiniteType.of_finiteType Module.Free.of_divisionRing IsArtinianRing.of_finite IsScalarTower.right isArtinian_of_fg_of_artinian' DivisionRing.instIsArtinianRing Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self Algebra.FormallyUnramified.isReduced_of_field IsArtinianRing.isField_of_isReduced_of_isLocalRing Localization.AtPrime.isLocalRing RingHom.injective DivisionRing.isSimpleRing EuclideanDomain.toNontrivial IsScalarTower.algebraMap_apply IsLocalRing.instIsScalarTowerResidueField Polynomial.aeval_algebraMap_apply OreLocalization.instIsScalarTower minpoly.aeval map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass IsLocalization.map_eq_zero_iff Localization.isLocalization pow_two mul_dvd_mul_iff_right Polynomial.instIsCancelMulZeroOfIsCancelAdd AddCancelMonoid.toIsCancelAdd IsDomain.toIsCancelMulZero instIsDomain minpoly.ne_zero Algebra.IsIntegral.isIntegral Algebra.IsAlgebraic.isIntegral Algebra.IsAlgebraic.of_finite IsLocalRing.instFiniteResidueField Dvd.dvd.trans NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Ideal.algebraMap_residueField_eq_zero minpoly.dvd_iff

---

← Back to Index