algEquivOfAlgEquiv_algebraMap — Mathlib

English

The fieldEquivOfAlgEquiv respects algebraMap on B, i.e., it maps algebraMap B FB b to algebraMap C FC (f b).

Русский

Полеэквивелентность fieldEquivOfAlgEquiv сохраняет algebraMap на B, переводя algebraMap B FB b в algebraMap C FC (f b).

LaTeX

$$$\text{fieldEquivOfAlgEquiv FA FB FC f} (\operatorname{algebraMap} B FB b) = \operatorname{algebraMap} C FC (f b)$$$

Lean4

@[simp]
theorem algEquivOfAlgEquiv_algebraMap (a : A) : algEquivOfAlgEquiv h (algebraMap A K a) = algebraMap B L (h a) := by
  simp [algEquivOfAlgEquiv]

Похожие утверждения