ringEquivOfRingEquiv_algebraMap — Mathlib

English

For a RingEquiv h between A and B, and a map algebraMap A K a, the value of ringEquivOfRingEquiv on algebraMap A K a equals algebraMap B L (h a).

Русский

Для RingEquiv h между A и B, значение ringEquivOfRingEquiv на algebraMap A K a равно algebraMap B L (h a).

LaTeX

$$$\text{ringEquivOfRingEquiv } h (\operatorname{algebraMap} A K a) = \operatorname{algebraMap} B L (h a)$$$

Lean4

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

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