TwoSidedIdeal.unit_mem_iff

Stream: Is there code for X?

[Edison Xie]

We have TwoSidedIdeal.one_mem_iff but do we have these two lemmas? If not should I PR them?

import Mathlib.RingTheory.TwoSidedIdeal.Lattice

lemma TwoSidedIdeal.unit_mem_iff {R : Type*} [Ring R] {I : TwoSidedIdeal R} {x : Rˣ}:
  x.1 ∈ I ↔ I = ⊤ := ⟨fun hx ↦ TwoSidedIdeal.one_mem_iff I|>.1 <| (Units.inv_mul x).symm ▸
    TwoSidedIdeal.mul_mem_left I _ _ hx, fun h ↦ by simp_all⟩

lemma TwoSidedIdeal.isUnit_mem_iff {R : Type*} [Ring R] {I : TwoSidedIdeal R} {x : R}
    (hx0 : IsUnit x) : x ∈ I ↔ I = ⊤ :=
  show hx0.unit.1 ∈ I ↔ _ from TwoSidedIdeal.unit_mem_iff

[Yaël Dillies]

@loogle IsUnit, TwoSidedIdeal

[Yaël Dillies]

says no

[Edison Xie]

Yaël Dillies said:

says no

do we want them?

[Edison Xie]

I'll make the PR then! :-)