coe_nsmul — Mathlib

English

The coercion of the natural-scalar multiple matches the natural-scalar multiple of the underlying submodule.

Русский

Приведение множителя на натуральную величину совпадает с соответствующим множителем на основанном подмодуле.

LaTeX

$$$↑(n \cdot I) = n \cdot (I)$$$

Lean4

@[norm_cast]
theorem coe_nsmul (n : ℕ) (I : FractionalIdeal S P) : (↑(n • I) : Submodule R P) = n • (I : Submodule R P) :=
  rfl

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