torsionBy_le_torsionBy_of_dvd — Mathlib

English

If a divides b, then the torsion by a is contained in the torsion by b: torsionBy(R, M, a) ≤ torsionBy(R, M, b) when a | b.

Русский

Если a делится на b (a|b), то торион по a содержится в торионе по b.

LaTeX

$$$\text{If } a \mid b, \quad \mathrm{torsionBy}\,R\,M\,a \leq \mathrm{torsionBy}\,R\,M\,b$$$

Lean4

theorem torsionBy_le_torsionBy_of_dvd (a b : R) (dvd : a ∣ b) : torsionBy R M a ≤ torsionBy R M b :=
  by
  rw [← torsionBySet_span_singleton_eq, ← torsionBySet_singleton_eq]
  apply torsionBySet_le_torsionBySet_of_subset
  rintro c (rfl : c = b); exact Ideal.mem_span_singleton.mpr dvd

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