instFaithfulSMul — Mathlib

English

The action of A/p on B/P is faithful; i.e. if ā acts trivially on all elements of B/P, then ā = 0 in A/p.

Русский

Действие A/p на B/P является верным (faithful); если элемент действует тривиально на каждом элементе B/P, тогда он равен нулю в A/p.

LaTeX

$$$ \\text{FaithfulSMul} (A/ p) (B/ P). $$$

Lean4

instance instFaithfulSMul : FaithfulSMul (A ⧸ p) (B ⧸ P) :=
  by
  rw [faithfulSMul_iff_algebraMap_injective]
  rintro ⟨a⟩ ⟨b⟩ hab
  apply Quotient.eq.mpr ((mem_of_liesOver P p (a - b)).mpr _)
  rw [RingHom.map_sub]
  exact Quotient.eq.mp hab

Похожие утверждения