English
There is a LocalizedModule instance for Submodule.toLocalizedQuotient p M′, i.e., Submodule.toLocalizedQuotient p M′ is a localized module with respect to p.
Русский
Существует экземпляр LocalizedModule для Submodule.toLocalizedQuotient p M′, т.е. Submodule.toLocalizedQuotient p M′ является локализованным модулем относительно p.
LaTeX
$$$\text{IsLocalizedModule } p \,(\mathrm{Submodule}.\mathrm{toLocalizedQuotient}\; p\ M')$$$
Lean4
/-- Define a `Module` structure on a Type by proving a minimized set of axioms. -/
abbrev ofMinimalAxioms {R : Type u} {M : Type v} [Semiring R] [AddCommGroup M]
[SMul R M]
-- Scalar multiplication distributes over addition from the left.
(smul_add : ∀ (r : R) (x y : M), r • (x + y) = r • x + r • y)
-- Scalar multiplication distributes over addition from the right.
(add_smul : ∀ (r s : R) (x : M), (r + s) • x = r • x + s • x)
-- Scalar multiplication distributes over multiplication from the right.
(mul_smul : ∀ (r s : R) (x : M), (r * s) • x = r • s • x)
-- Scalar multiplication by one is the identity.
(one_smul : ∀ x : M, (1 : R) • x = x) : Module R M :=
{ smul_add := smul_add, add_smul := add_smul, mul_smul := mul_smul, one_smul := one_smul,
zero_smul := fun x => (AddMonoidHom.mk' (· • x) fun r s => add_smul r s x).map_zero
smul_zero := fun r => (AddMonoidHom.mk' (r • ·) (smul_add r)).map_zero }
