Coordinates in the basis of G / nG #
For a ℤ-basis b of a free ℤ-module G and n ≠ 0, Mathlib's ModN.basis b is the basis of
ModN G n = G / nG over ℤ / n formed by the classes of the vectors of b. This file records
that the coordinates of the class of v in this basis are the coordinates of v in b, reduced
modulo n.
Main statements #
ModN.basis_repr_mkQ,ModN.basis_repr_mk:(ModN.basis b).repr [v] i = (b.repr v i : ℤ / n).
@[simp]
theorem
ModN.basis_repr_mkQ
{G : Type u_1}
{ι : Type u_2}
[AddCommGroup G]
{n : ℕ}
[NeZero n]
(b : Module.Basis ι ℤ G)
(v : G)
(i : ι)
:
The coordinates of the class of v in ModN.basis b are the coordinates of v in b,
reduced modulo n.
@[simp]
theorem
ModN.basis_repr_mk
{G : Type u_1}
{ι : Type u_2}
[AddCommGroup G]
{n : ℕ}
[NeZero n]
(b : Module.Basis ι ℤ G)
(v : G)
(i : ι)
:
The coordinates of the class of v in ModN.basis b are the coordinates of v in b,
reduced modulo n: the form of ModN.basis_repr_mkQ for Submodule.Quotient.mk.