add_circle): define the additive circle (#16201)

Commit

3 years ago

feat(analysis/normed/group/add_circle): define the additive circle (#16201) Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>

Author

ocfnash

Parents

08bb56fb

mathlib3 ebe6bda5 - feat(analysis/normed/group/add_circle): define the additive circle (#16201)

mathlib3
ebe6bda5 - feat(analysis/normed/group/add_circle): define the additive circle (#16201)