Theorems · Theorem · field theory

Subfield.map_map

∀ {K : Type u} {L : Type v} {M : Type w} [inst : DivisionRing K] [inst_1 : DivisionRing L] [inst_2 : DivisionRing M]
  (s : Subfield K) (g : L →+* M) (f : K →+* L), Subfield.map g (Subfield.map f s) = Subfield.map (g.comp f) s

Defined in

Mathlib.Algebra.Field.Subfield.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

DivisionRingDivisionRingDivisionRing