smul_toInvSubmonoid — Mathlib

English

In the localization, the product of algebraMap(R,S)(m) with its inverse image equals 1.

Русский

В локализации произведение образа из R в S и его обратного образа равно 1.

LaTeX

$$$(algebraMap\ R\ S\ m) \cdot (toInvSubmonoid\ M\ S\ m : S) = 1$$$

Lean4

@[simp]
theorem smul_toInvSubmonoid (m : M) : m • (toInvSubmonoid M S m : S) = 1 :=
  by
  convert mul_toInvSubmonoid M S m
  ext
  rw [← Algebra.smul_def]
  rfl

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