English
Consider A,B,C with appropriate rings and modules, then for any submodule I of Balo C, and n ≠ 0, I^n restricted to A equals I.restrictScalars A^n.
Русский
Пусть имеют место подходящие кольца и модули; для подмодуля I ⊆ B C верно: I^n, ограниченный скалярами A, равен I, ограниченному по A, возведённому в степень n (при n≠0).
LaTeX
$$$ \forall {I : Submodule B C}, \; Ne n 0 → I^{n} \restrictScalars A = I.\restrictScalars A^{n}. $$$
Lean4
theorem restrictScalars_pow {A B C : Type*} [Semiring A] [Semiring B] [Semiring C] [SMul A B] [Module A C] [Module B C]
[IsScalarTower A C C] [IsScalarTower B C C] [IsScalarTower A B C] {I : Submodule B C} :
∀ {n : ℕ}, (hn : n ≠ 0) → (I ^ n).restrictScalars A = I.restrictScalars A ^ n
| 1, _ => by simp [Submodule.pow_one]
| n + 2, _ => by simp [Submodule.pow_succ (n := n + 1), restrictScalars_mul, restrictScalars_pow n.succ_ne_zero]
