English
If a ring A has a family B: ι → AddSubgroup A with compatible intersections, multiplicative closure, and left-multiplication behavior, then B forms a RingSubgroupsBasis.
Русский
Если кольцо A имеет семейство B: ι → AddSubgroup A, удовлетворяющее условиям совместности пересечений, замкнутости при умножении и левого умножения, тогда B образует RingSubgroupsBasis.
LaTeX
$$The three conditions (inter, mul, leftMul) imply RingSubgroupsBasis B.$$
Lean4
theorem of_comm {A ι : Type*} [CommRing A] (B : ι → AddSubgroup A) (inter : ∀ i j, ∃ k, B k ≤ B i ⊓ B j)
(mul : ∀ i, ∃ j, (B j : Set A) * B j ⊆ B i)
(leftMul : ∀ x : A, ∀ i, ∃ j, (B j : Set A) ⊆ (fun y : A => x * y) ⁻¹' B i) : RingSubgroupsBasis B :=
{ inter
mul
leftMul
rightMul := fun x i ↦ (leftMul x i).imp fun j hj ↦ by simpa only [mul_comm] using hj }
