Theorems · Definition · ring theory
AlgEquiv.ofInjectiveField
{R : Type u} →
[inst : CommSemiring R] →
{E : Type u_1} →
{F : Type u_2} →
[inst_1 : DivisionRing E] →
[inst_2 : Semiring F] →
[Nontrivial F] → [inst_4 : Algebra R E] → [inst_5 : Algebra R F] → (f : E →ₐ[R] F) → E ≃ₐ[R] ↥f.rangeRestrict an algebra homomorphism between fields to an algebra isomorphism
- Defined in
- Mathlib.Algebra.Algebra.Subalgebra.Basic
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 55 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- AlgHomstatement and proof · cited by 3,236
- Nontrivialstatement and proof · cited by 2,416
- AlgEquivstatement · cited by 1,681
- Subalgebrastatement · cited by 1,353
- DivisionRingstatement and proof · cited by 1,062
- AlgHom.rangestatement · cited by 169
- AlgEquiv.ofInjectiveproof · cited by 16
Cited by23
Results whose statement or proof uses this declaration.
- AlgHom.restrictNormal_commutesproof · cited by 9
- IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraicproof · cited by 5
- AlgebraicIndependent.aevalEquivFieldproof · cited by 5
- AlgHom.restrictNormalproof · cited by 4
- IntermediateField.restrictAlgEquivproof · cited by 2
- IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraicproof · cited by 2
- IntermediateField.exists_algHom_adjoin_of_splits'proof · cited by 1
- IntermediateField.LinearDisjoint.of_basis_leftproof · cited by 1
- FunctionField.finiteDimensional_ratFunc_of_constantExtensionproof · cited by 1
- IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_isSepClosedproof · cited by 1