case zero
R : Type u
ι : Type ?u.225378
inst✝ : CommSemiring R
I J K L : Ideal R
s : R
⊢ span {s} ^ Nat.zero = span {s ^ Nat.zero}

case succ
R : Type u
ι : Type ?u.225378
inst✝ : CommSemiring R
I J K L : Ideal R
s : R
n : ℕ
ih : span {s} ^ n = span {s ^ n}
⊢ span {s} ^ Nat.succ n = span {s ^ Nat.succ n}
R : Type u
ι : Type ?u.225378
inst✝ : CommSemiring R
I J K L : Ideal R
s : R
n : ℕ
⊢ span {s} ^ n = span {s ^ n}
induction' n with n ih
no goals
case succ
R : Type u
ι : Type ?u.225378
inst✝ : CommSemiring R
I J K L : Ideal R
s : R
n : ℕ
ih : span {s} ^ n = span {s ^ n}
⊢ span {s} ^ Nat.succ n = span {s ^ Nat.succ n}
simp only [pow_succ, ih, span_singleton_mul_span_singleton]
no goals
case zero
R : Type u
ι : Type ?u.225378
inst✝ : CommSemiring R
I J K L : Ideal R
s : R
⊢ span {s} ^ Nat.zero = span {s ^ Nat.zero}
simp [Set.singleton_one]