instSMulNat

Mathlib.RingTheory.FractionalIdeal.Basic

URI: https://scilib.ai/kg/mathlib#FractionalIdeal.instSMulNat

English

If I is a fractional submodule, then all its natural powers I^n are fractional for all n ∈ N.

Русский

Если I – дробный подмодуль, то все его натуральные степени I^n являются дробными для всех n ∈ N.

LaTeX

$$$IsFractional S I \to \forall n \in \mathbb{N}, IsFractional S (I^n)$$$

Lean4

instance : SMul ℕ (FractionalIdeal S P) where smul n I := ⟨n • ↑I, I.isFractional.nsmul n⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru