coe_ofDense — Mathlib

English

The underlying function of the dense extension MulHom.ofDense equals the original function f.

Русский

Кульминация функционала плотного расширения MulHom.ofDense совпадает с исходной функцией f.

LaTeX

$$$(\\mathrm{ofDense}\, f\, hs\, hmul : M \\to N) = f$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_ofDense [Semigroup M] [Semigroup N] {s : Set M} (f : M → N) (hs : closure s = ⊤) (hmul) :
    (ofDense f hs hmul : M → N) = f :=
  rfl

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