Theorems · Theorem · commutative algebra

Module.Basis.SmithNormalForm.repr_apply_embedding_eq_repr_smul

∀ {ι : 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) (m : ↥N) {i : Fin n},
  (snf.bM.repr ↑m) (snf.f i) = (snf.bN.repr (snf.a i • m)) i

Defined in: Mathlib.LinearAlgebra.FreeModule.PID
Cited by: 3 results in Mathlib
Foundations: Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing AddCommGroup Module

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites32

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Modulestatement and proof · cited by 20,661
RingHom.idstatement · cited by 18,349
CommRingstatement and proof · cited by 17,173
AddCommGroupstatement and proof · cited by 12,871
Submodulestatement and proof · cited by 7,192
Finsuppstatement and proof · cited by 5,255
mul_oneproof · cited by 3,885
LinearEquivstatement · cited by 3,317
mul_commproof · cited by 2,262
Function.Embeddingstatement · cited by 988
Finsupp.singleproof · cited by 943

Cited by3

Results whose statement or proof uses this declaration.

Module.Basis.SmithNormalForm.toMatrix_restrict_eq_toMatrixproof · cited by 1
Module.Basis.SmithNormalForm.coord_apply_embedding_eq_smul_coordproof · cited by 0
Module.Basis.SmithNormalForm.repr_comp_embedding_eq_smulproof · cited by 0