∀ {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Submodule R M}
  {ι : Type u_4} {n : ℕ} (self : Module.Basis.SmithNormalForm N ι n) (i : Fin n),
  ↑(self.bN i) = self.a i • self.bM (self.f i)