torsionBySet_univ — Mathlib

English

The torsion by all scalars is trivial: torsionBySet(R, M, Set.univ) = ⊥.

Русский

Торион по всем скалярам тривиален: torsionBySet(R, M, Set.univ) = ⊥.

LaTeX

$$$\mathrm{torsionBySet}\,R\,M\,\mathrm{Set.univ} = \bot$$$

Lean4

@[simp]
theorem torsionBySet_univ : torsionBySet R M Set.univ = ⊥ :=
  by
  rw [eq_bot_iff, ← torsionBy_one, ← torsionBySet_singleton_eq]
  exact torsionBySet_le_torsionBySet_of_subset fun _ _ => trivial

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