mem_grade_iff' — Mathlib

English

Remainder of basis element by itself is zero.

Русский

Остаток базисного элемента по самого себя равен нулю.

LaTeX

$$$ \\operatorname{of}'(g) \\bmod^{\\circ} g = 0 $$$

Lean4

theorem mem_grade_iff' (m : M) (a : R[M]) :
    a ∈ grade R m ↔ a ∈ (LinearMap.range (Finsupp.lsingle m : R →ₗ[R] M →₀ R) : Submodule R R[M]) :=
  by
  rw [mem_grade_iff, Finsupp.support_subset_singleton']
  apply exists_congr
  intro r
  constructor <;> exact Eq.symm

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