have H := Basis.sum_repr pb.basis x
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H : ∑ i : Fin pb.dim, (pb.basis.repr x) i • pb.basis i = x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]