coe_pow — Mathlib

English

Coefficient-wise power of a fractional ideal equals the power of its underlying submodule, i.e., the coe to submodule commutes with HPow^n.

Русский

Сопоставление коэффициентов к степеням дробного идеала совпадает со степенью соответствующего подмодуля.

LaTeX

$$$\uparrow(I^n) = (\uparrow I)^n$$$

Lean4

@[simp, norm_cast]
theorem coe_pow (I : FractionalIdeal S P) (n : ℕ) : ↑(I ^ n) = (I : Submodule R P) ^ n :=
  rfl

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