smul_mem_iff — Mathlib

English

Congruence of AlgEquivOfAlgEquiv across equivalent monoid maps.

Русский

Согласованность AlgEquivOfAlgEquiv при эквивалентных отображениях моноидов.

LaTeX

$$$\\mathrm{IsLocalization.algEquivOfAlgEquiv}(S,Q,h,H) = \\mathrm{IsLocalization.algEquivOfAlgEquiv}(S,Q,h',H')$$$

Lean4

/-- If `x` in a `R' = S⁻¹ R`-module `M'`, then for a submodule `N'` of `M'`,
`s • x ∈ N'` if and only if `x ∈ N'` for some `s` in S. -/
theorem smul_mem_iff {N' : Submodule R' M'} {x : M'} {s : S} : s • x ∈ N' ↔ x ∈ N' :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ Submodule.smul_of_tower_mem N' s h⟩
  rwa [← Submodule.smul_mem_iff_of_isUnit (r := algebraMap R R' s) N' (map_units R' s), algebraMap_smul]

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