English
When A is a Semiring and LocalizedModule S A is formed, the localization carries a semiring structure where addition distributes over multiplication from both sides, and zero acts as the absorbing element.
Русский
Когда A — полупрямое кольцо и образуется локализованный модуль LocalizedModule S A, локализация имеет структуру полугруппы с распределением, где сложение распределяется по умножению слева и справа, ноль поглощает.
LaTeX
$$$\\mathrm{LocalizedModule}(S,A)$ is a Semiring with distributive laws$$
Lean4
instance {A : Type*} [Semiring A] [Algebra R A] {S : Submonoid R} : Semiring (LocalizedModule S A) :=
{ show (AddCommMonoid (LocalizedModule S A)) by infer_instance,
show (Monoid (LocalizedModule S A)) by
infer_instance with
left_distrib := by
rintro ⟨a₁, s₁⟩ ⟨a₂, s₂⟩ ⟨a₃, s₃⟩
apply mk_eq.mpr _
use 1
simp only [one_mul, smul_add, mul_add, mul_smul_comm, smul_smul, ← mul_assoc, mul_right_comm]
right_distrib := by
rintro ⟨a₁, s₁⟩ ⟨a₂, s₂⟩ ⟨a₃, s₃⟩
apply mk_eq.mpr _
use 1
simp only [one_mul, smul_add, add_mul, smul_smul, ← mul_assoc, smul_mul_assoc, mul_right_comm]
zero_mul := by
rintro ⟨a, s⟩
exact mk_eq.mpr ⟨1, by simp only [zero_mul, smul_zero]⟩
mul_zero := by
rintro ⟨a, s⟩
exact mk_eq.mpr ⟨1, by simp only [mul_zero, smul_zero]⟩ }
