Theorems · Theorem · commutative algebra

Module.Basis.SmithNormalForm.coord_apply_embedding_eq_smul_coord

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

Defined in

Mathlib.LinearAlgebra.FreeModule.PID

Cited by

0 results in Mathlib

Foundations

Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModule