mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Operations
Submodule.restrictScalars_pow : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Semiring A] [inst_1 : Semiring B] [inst_2 : Semiring C]
  [inst_3 : SMul A B] [inst_4 : Module A C] [inst_5 : Module B C] [inst_6 : IsScalarTower A C C]
  [inst_7 : IsScalarTower B C C] [inst_8 : IsScalarTower A B C] {I : Submodule B C} {n : ℕ},
  n ≠ 0 → Submodule.restrictScalars A (I ^ n) = Submodule.restrictScalars A I ^ n