Theorems · Theorem · field theory

Subfield.closure_preimage_le

∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (f : K →+* L) (s : Set L),
  Subfield.closure (⇑f ⁻¹' s) ≤ Subfield.comap f (Subfield.closure s)

Defined in

Mathlib.Algebra.Field.Subfield.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

DivisionRingDivisionRing