ext' — Mathlib

English

If two R-module structures P and Q on the same underlying abelian group M have identical scalar actions, then P = Q.

Русский

Если две структуры модуля над R на одном и том же абелевой группе M совпадают по скалярному действию, то P = Q.

LaTeX

$$$\\forall r \\in R, \\forall m \\in M, r \\cdot_P m = r \\cdot_Q m \\Rightarrow P = Q$$$

Lean4

/-- A variant of `Module.ext` that's convenient for term-mode. -/
theorem ext' {R : Type*} [Semiring R] {M : Type*} [AddCommMonoid M] (P Q : Module R M)
    (w :
      ∀ (r : R) (m : M),
        (haveI := P;
          r • m) =
          (haveI := Q;
          r • m)) :
    P = Q := by
  ext
  exact w _ _

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