Skip to content

Commit

Permalink
doc: tidy the docstring of Subgroup.centralizer (#20365)
Browse files Browse the repository at this point in the history
The argument is now named `s` as it has type `Set G` (not `Subgroup G`)
  • Loading branch information
ldct committed Jan 1, 2025
1 parent 7178aee commit bd681bc
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Mathlib/GroupTheory/Subgroup/Centralizer.lean
Original file line number Diff line number Diff line change
Expand Up @@ -17,9 +17,9 @@ namespace Subgroup

variable {H K : Subgroup G}

/-- The `centralizer` of `H` is the subgroup of `g : G` commuting with every `h : H`. -/
/-- The `centralizer` of `s` is the subgroup of `g : G` commuting with every `h : s`. -/
@[to_additive
"The `centralizer` of `H` is the additive subgroup of `g : G` commuting with every `h : H`."]
"The `centralizer` of `s` is the additive subgroup of `g : G` commuting with every `h : s`."]
def centralizer (s : Set G) : Subgroup G :=
{ Submonoid.centralizer s with
carrier := Set.centralizer s
Expand Down

0 comments on commit bd681bc

Please sign in to comment.