Field

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

Statistics

Metric	Count
Definitions	0
Theorems iff_exists_algEquiv_prod, iff_exists_algEquiv_prod, iff_formallyUnramified_of_field, iff_isSeparable, of_formallyUnramified_of_field, of_isSeparable, of_isSeparable_aux	7
Total	7

Algebra.Etale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_exists_algEquiv_prod 📖	mathematical	—	Algebra.Etale EuclideanDomain.toCommRing Field.toEuclideanDomain Module.Finite DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Semifield.toCommSemiring Algebra.IsSeparable DivisionRing.toRing Field.toDivisionRing	—	Algebra.FormallyEtale.iff_exists_algEquiv_prod Algebra.EssFiniteType.of_finiteType Algebra.FiniteType.of_finitePresentation finitePresentation formallyEtale Algebra.FormallyUnramified.finite_of_free Algebra.FormallyEtale.instFormallyUnramified Module.Free.of_divisionRing Module.Finite.of_surjective RingHomSurjective.ids RingHomCompTriple.ids Function.surjective_eval Nontrivial.to_nonempty IsLocalRing.toNontrivial Field.instIsLocalRing AlgEquiv.surjective FiniteDimensional.finiteDimensional_pi' Module.Finite.finiteType Algebra.FinitePresentation.of_finiteType IsSimpleModule.instIsNoetherian instIsSimpleModule

Algebra.FormallyEtale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_exists_algEquiv_prod 📖	mathematical	—	Algebra.FormallyEtale EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.IsSeparable DivisionRing.toRing Field.toDivisionRing	—	Algebra.FormallyUnramified.finite_of_free instFormallyUnramified Module.Free.of_divisionRing Algebra.FormallyUnramified.isReduced_of_field isArtinian_of_tower IsScalarTower.right isArtinian_of_fg_of_artinian' DivisionRing.instIsArtinianRing IsArtinianRing.instFiniteMaximalSpectrum Pi.isScalarTower Ideal.Quotient.isScalarTower iff_isSeparable Algebra.instEssFiniteTypeQuotientIdeal pi_iff iff_of_equiv of_isSeparable
iff_formallyUnramified_of_field 📖	mathematical	—	Algebra.FormallyEtale EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.FormallyUnramified	—	instFormallyUnramified of_formallyUnramified_of_field
iff_isSeparable 📖	mathematical	—	Algebra.FormallyEtale EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.IsSeparable DivisionRing.toRing Field.toDivisionRing	—	Algebra.FormallyUnramified.isSeparable instFormallyUnramified of_isSeparable
of_formallyUnramified_of_field 📖	mathematical	—	Algebra.FormallyEtale EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Algebra.FormallyUnramified.isReduced_of_field IsArtinianRing.of_finite IsScalarTower.right isArtinian_of_fg_of_artinian' DivisionRing.instIsArtinianRing Algebra.FormallyUnramified.finite_of_free Algebra.FormallyUnramified.inst Algebra.EssFiniteType.of_finiteType Algebra.FiniteType.of_finitePresentation Algebra.FinitePresentation.self Module.Free.self Module.Free.of_divisionRing MaximalSpectrum.isMaximal iff_isSeparable Algebra.instEssFiniteTypeQuotientIdeal Algebra.FormallyUnramified.iff_isSeparable Algebra.FormallyUnramified.quotient of_equiv instForallOfFinite IsArtinianRing.instFiniteMaximalSpectrum Pi.isScalarTower Ideal.Quotient.isScalarTower
of_isSeparable 📖	mathematical	—	Algebra.FormallyEtale EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Ideal.instIsTwoSided_1 iff_comp_bijective Algebra.FormallyUnramified.iff_comp_injective_of_small UnivLE.small univLE_of_max UnivLE.self Algebra.FormallyUnramified.of_isSeparable IsScalarTower.left SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IntermediateField.isScalarTower_mid' Algebra.IsSeparable.of_algHom IntermediateField.adjoin.finiteDimensional IsSeparable.isIntegral Algebra.IsSeparable.isSeparable of_isSeparable_aux Algebra.EssFiniteType.of_finiteType Module.Finite.finiteType comp_bijective Function.Bijective.existsUnique IntermediateField.adjoin_le_iff AlgHom.ext AlgHom.comp_assoc IntermediateField.finiteDimensional_adjoin Finite.Set.finite_insert Finite.of_fintype Field.exists_primitive_element IntermediateField.subset_adjoin Set.image_congr Set.image_singleton IntermediateField.fieldRange_val AlgHom.fieldRange_eq_map IntermediateField.adjoin_map AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubsemiringClass.toSubmonoidClass NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass map_zero MonoidWithZeroHomClass.toZeroHomClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.commutes AlgHom.congr_fun
of_isSeparable_aux 📖	mathematical	—	Algebra.FormallyEtale EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Algebra.FormallyUnramified.of_isSeparable Algebra.FormallyUnramified.finite_of_free Module.Free.of_divisionRing Ideal.instIsTwoSided_1 iff_comp_bijective Algebra.FormallyUnramified.iff_comp_injective_of_small UnivLE.small univLE_of_max UnivLE.self Ideal.Quotient.mk_surjective Ideal.Quotient.isScalarTower IsScalarTower.right Polynomial.aeval_algHom_apply AlgHom.algHomClass minpoly.aeval map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass isUnit_iff_ne_zero Polynomial.Separable.aeval_derivative_ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing Algebra.IsSeparable.isSeparable Ideal.Quotient.eq_zero_iff_mem map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_one MonoidHomClass.toOneHomClass mul_neg IsUnit.mul_val_inv neg_add_cancel Polynomial.eval_map_algebraMap Polynomial.eval_add_of_sq_eq_zero Ideal.mem_bot Ideal.pow_mem_pow MulZeroClass.mul_zero Polynomial.derivative_map one_mul mul_assoc add_mul Distrib.rightDistribClass pow_two add_comm Ideal.mul_mem_mul PowerBasis.algHom_ext PowerBasis.lift_gen add_zero

---

← Back to Index