feat(group_theory/nilpotent): add antimono and functorial lemma for lower central series (#8853)
feat(group_theory/nilpotent): add antimono and functorial lemma for lower central series (#8853)




Co-authored-by: ineswright <e319c41fcb6f78c4337bc6ea37561a1c7d3f9b2d@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib