Theorems · Definition · field theory

Subfield.comap

{K : Type u} → {L : Type v} → [inst : DivisionRing K] → [inst_1 : DivisionRing L] → (K →+* L) → Subfield L → Subfield K

The preimage of a subfield along a ring homomorphism is a subfield.

Defined in

Mathlib.Algebra.Field.Subfield.Basic

Cited by

29 results in Mathlib

Foundations

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

Assumes

DivisionRingDivisionRing