coe_congrOrderIso_apply — Mathlib

English

Applying congrOrderIso and then coercing to MulArchimedeanClass N yields the same as applying e to a.

Русский

Применение congrOrderIso и последующая коэрцизация к MulArchimedeanClass N эквивалентны применению e к a.

LaTeX

$$$(congrOrderIso e)\; a = e a$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_congrOrderIso_apply (e : MulArchimedeanClass M ≃o MulArchimedeanClass N) (a : FiniteMulArchimedeanClass M) :
    (congrOrderIso e a : MulArchimedeanClass N) = e a :=
  rfl

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