Centralizer

Stream: Is there code for X?

[Li Xuanji]

Are either of these theorems? I found le_normalizer but nothing for these.

import Mathlib

example (G : Type) [Group G] (A : Subgroup G) : Subgroup.centralizer A ≤ Subgroup.normalizer A := by
  sorry

example (G : Type) [Group G] (A : Subgroup G) : A ≤ Subgroup.centralizer A := by
  sorry

[Kim Morrison]

The second one is only true for G commutative.

[Kim Morrison]

That said I'm failing to find either.

[Yaël Dillies]

Surely both statements are a bit silly when G is commutative, since the centralizer and normalizer are everything?

[Yaël Dillies]

Oh, you probably meant "when A is commutative", sorry

[Kim Morrison]

Oops, sorry. Something had better be commutative! :-)

[Jz Pan]

@loogle Subgroup.centralizer, Subgroup.normalizer, |- LE.le ..

[loogle]

:shrug: nothing found