From 43fb516261d5d82dde3bd5cd381653888b212001 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sat, 26 Feb 2022 02:44:14 +0000 Subject: [PATCH] doc(analysis/normed_space): fixed normed_star_monoid doc-string (#12296) Co-authored-by: Scott Morrison --- src/analysis/normed_space/star/basic.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/analysis/normed_space/star/basic.lean b/src/analysis/normed_space/star/basic.lean index cd21a6db12e87..e6c64dd514a7d 100644 --- a/src/analysis/normed_space/star/basic.lean +++ b/src/analysis/normed_space/star/basic.lean @@ -35,7 +35,8 @@ open_locale topological_space local postfix `⋆`:std.prec.max_plus := star -/-- A normed star ring is a star ring endowed with a norm such that `star` is isometric. -/ +/-- A normed star monoid is an additive monoid with a star, +endowed with a norm such that `star` is isometric. -/ class normed_star_monoid (E : Type*) [normed_group E] [star_add_monoid E] : Prop := (norm_star : ∀ {x : E}, ∥x⋆∥ = ∥x∥)