Theorems · Theorem · field theory
Algebra.IsSeparable.of_equiv_equiv
∀ {A₁ : Type u_1} {B₁ : Type u_2} {A₂ : Type u_3} {B₂ : Type u_4} [inst : Field A₁] [inst_1 : Ring B₁]
[inst_2 : Field A₂] [inst_3 : Ring B₂] [inst_4 : Algebra A₁ B₁] [inst_5 : Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂)
(e₂ : B₁ ≃+* B₂),
(algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁) → ∀ [Algebra.IsSeparable A₁ B₁], Algebra.IsSeparable A₂ B₂- Defined in
- Mathlib.FieldTheory.Separable
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 124 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Algebrastatement and proof · cited by 11,388
- RingHomstatement · cited by 10,189
- Ringstatement and proof · cited by 7,463
- Fieldstatement and proof · cited by 7,404
- Algebra.algebraMapstatement and proof · cited by 4,706
- RingEquivstatement and proof · cited by 1,147
- RingHom.compstatement and proof · cited by 899
- RingHomClass.toRingHomstatement and proof · cited by 746
- RingEquiv.symmproof · cited by 567
- Algebra.IsSeparablestatement and proof · cited by 210
- RingEquiv.apply_symm_applyproof · cited by 53
Cited by6
Results whose statement or proof uses this declaration.
- Algebra.IsSeparable.iff_of_equiv_equivproof · cited by 1
- IsDedekindDomain.differentIdeal_dvd_map_differentIdealproof · cited by 1
- IsGalois.of_equiv_equivproof · cited by 1
- coeSubmodule_differentIdealproof · cited by 1
- FractionRing.isSeparable_of_isLocalizationproof · cited by 0
- Submodule.traceDual_eq_span_map_traceDual_of_linearDisjointproof · cited by 0