Lean4
/-- Every subgroups basis on a ring leads to a ring filter basis. -/
def toRingFilterBasis [Nonempty ι] {B : ι → AddSubgroup A} (hB : RingSubgroupsBasis B) : RingFilterBasis A
where
sets := {U | ∃ i, U = B i}
nonempty := by
inhabit ι
exact ⟨B default, default, rfl⟩
inter_sets := by
rintro _ _ ⟨i, rfl⟩ ⟨j, rfl⟩
obtain ⟨k, hk⟩ := hB.inter i j
use B k
constructor
· use k
· exact hk
zero' := by
rintro _ ⟨i, rfl⟩
exact (B i).zero_mem
add' := by
rintro _ ⟨i, rfl⟩
use B i
constructor
· use i
· rintro x ⟨y, y_in, z, z_in, rfl⟩
exact (B i).add_mem y_in z_in
neg' := by
rintro _ ⟨i, rfl⟩
use B i
constructor
· use i
· intro x x_in
exact (B i).neg_mem x_in
conj' := by
rintro x₀ _ ⟨i, rfl⟩
use B i
constructor
· use i
· simp
mul' := by
rintro _ ⟨i, rfl⟩
obtain ⟨k, hk⟩ := hB.mul i
use B k
constructor
· use k
· exact hk
mul_left' := by
rintro x₀ _ ⟨i, rfl⟩
obtain ⟨k, hk⟩ := hB.leftMul x₀ i
use B k
constructor
· use k
· exact hk
mul_right' := by
rintro x₀ _ ⟨i, rfl⟩
obtain ⟨k, hk⟩ := hB.rightMul x₀ i
use B k
constructor
· use k
· exact hk
