coe_ofLexMulEquiv — Mathlib

English

The coercion from Lex MulEquiv matches the standard embedding; the two ways of viewing the map agree.

Русский

Связь между двумя способами вклинения в Lex MulEquiv совпадает; коэффициентная карта совпадает с обычной вставкой.

LaTeX

$$$\text{coe}((\mathrm{ofLexMulEquiv} \alpha)) = \text{coe}(\mathrm{ofLex})$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_ofLexMulEquiv : ⇑(ofLexMulEquiv α) = ofLex :=
  rfl

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