Theorems · Theorem · commutative algebra

RingFilterBasis.mk.congr_simp

∀ {R : Type u} [inst : Ring R] [toAddGroupFilterBasis : AddGroupFilterBasis R]
  [toAddGroupFilterBasis_1 : AddGroupFilterBasis R]
  (e_toAddGroupFilterBasis : toAddGroupFilterBasis = toAddGroupFilterBasis_1)
  (mul' : ∀ {U : Set R}, U ∈ toAddGroupFilterBasis.sets → ∃ V ∈ toAddGroupFilterBasis.sets, V * V ⊆ U)
  (mul_left' :
    ∀ (x₀ : R) {U : Set R},
      U ∈ toAddGroupFilterBasis.sets → ∃ V ∈ toAddGroupFilterBasis.sets, V ⊆ (fun x => x₀ * x) ⁻¹' U)
  (mul_right' :
    ∀ (x₀ : R) {U : Set R},
      U ∈ toAddGroupFilterBasis.sets → ∃ V ∈ toAddGroupFilterBasis.sets, V ⊆ (fun x => x * x₀) ⁻¹' U),
  { toAddGroupFilterBasis := toAddGroupFilterBasis, mul' := mul', mul_left' := mul_left', mul_right' := mul_right' } =
    { toAddGroupFilterBasis := toAddGroupFilterBasis_1, mul' := ⋯, mul_left' := ⋯, mul_right' := ⋯ }

Defined in

Mathlib.RingTheory.AdicCompletion.Topology

Cited by

1 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms

Assumes

RingAddGroupFilterBasisAddGroupFilterBasis