Theorems · Theorem · field theory

Algebra.IsSeparable.iff_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

1 results in Mathlib

Foundations

Depth 125 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldRingFieldRingAlgebraAlgebra