# Group seminorms #

This file defines norms and seminorms in a group. A group seminorm is a function to the reals which is positive-semidefinite and subadditive. A norm further only maps zero to zero.

## Main declarations #

- `AddGroupSeminorm`: A function `f` from an additive group `G` to the reals that preserves zero, takes nonnegative values, is subadditive and such that `f (-x) = f x` for all `x`.
- `NonarchAddGroupSeminorm`: A function `f` from an additive group `G` to the reals that preserves zero, takes nonnegative values, is nonarchimedean and such that `f (-x) = f x` for all `x`.
- `GroupSeminorm`: A function `f` from a group `G` to the reals that sends one to zero, takes nonnegative values, is submultiplicative and such that `f x⁻¹ = f x` for all `x`.
- `AddGroupNorm`: A seminorm `f` such that `f x = 0 → x = 0` for all `x`.
- `NonarchAddGroupNorm`: A nonarchimedean seminorm `f` such that `f x = 0 → x = 0` for all `x`.
- `GroupNorm`: A seminorm `f` such that `f x = 0 → x = 1` for all `x`.

## Notes #

The corresponding hom classes are defined in `Analysis.Order.Hom.Basic` to be used by absolute values.

We do not define `NonarchAddGroupSeminorm` as an extension of `AddGroupSeminorm` to avoid having a superfluous `add_le'` field in the resulting structure. The same applies to `NonarchAddGroupNorm`.

## References #

- [H. H. Schaefer, Topological Vector Spaces][schaefer1966]

## Tags #

norm, seminorm

source
structure AddGroupSeminorm (G : Type u_6) [AddGroup G] :
Type u_6

A seminorm on an additive group `G` is a function `f : G → ℝ` that preserves zero, is subadditive and such that `f (-x) = f x` for all `x`.

- toFun : G → ℝ

  The bare function of an `AddGroupSeminorm`.

- map_zero' : self.toFun 0 = 0

  The image of zero is zero.

- add_le' (r s : G) : self.toFun (r + s) ≤ self.toFun r + self.toFun s

  The seminorm is subadditive.

- neg' (r : G) : self.toFun (-r) = self.toFun r

  The seminorm is invariant under negation.

Instances For

source
structure GroupSeminorm (G : Type u_6) [Group G] :
Type u_6

A seminorm on a group `G` is a function `f : G → ℝ` that sends one to zero, is submultiplicative and such that `f x⁻¹ = f x` for all `x`.

- toFun : G → ℝ

  The bare function of a `GroupSeminorm`.

- map_one' : self.toFun 1 = 0

  The image of one is zero.

- mul_le' (x y : G) : self.toFun (x * y) ≤ self.toFun x + self.toFun y

  The seminorm applied to a product is dominated by the sum of the seminorm applied to the factors.

- inv' (x : G) : self.toFun x⁻¹ = self.toFun x

  The seminorm is invariant under inversion.

Instances For

source
structure NonarchAddGroupSeminorm (G : Type u_6) [AddGroup G] extends ZeroHom G ℝ :
Type u_6

A nonarchimedean seminorm on an additive group `G` is a function `f : G → ℝ` that preserves zero, is nonarchimedean and such that `f (-x) = f x` for all `x`.

- toFun : G → ℝ
- map_zero' : self.toFun 0 = 0
- add_le_max' (r s : G) : self.toFun (r + s) ≤ max (self.toFun r) (self.toFun s)

  The seminorm applied to a sum is dominated by the maximum of the function applied to the addends.

- neg' (r : G) : self.toFun (-r) = self.toFun r

  The seminorm is invariant under negation.

Instances For

NOTE: We do not define `NonarchAddGroupSeminorm` as an extension of `AddGroupSeminorm` to avoid having a superfluous `add_le'` field in the resulting structure. The same applies to `NonarchAddGroupNorm` below.

source
structure AddGroupNorm (G : Type u_6) [AddGroup G] extends AddGroupSeminorm G :
Type u_6

A norm on an additive group `G` is a function `f : G → ℝ` that preserves zero, is subadditive and such that `f (-x) = f x` and `f x = 0 → x = 0` for all `x`.

- toFun : G → ℝ
- map_zero' : self.toFun 0 = 0
- add_le' (r s : G) : self.toFun (r + s) ≤ self.toFun r + self.toFun s
- neg' (r : G) : self.toFun (-r) = self.toFun r
- eq_zero_of_map_eq_zero' (x : G) : self.toFun x = 0 → x = 0

  If the image under the seminorm is zero, then the argument is zero.

Instances For

source
structure GroupNorm (G : Type u_6) [Group G] extends GroupSeminorm G :
Type u_6

A seminorm on a group `G` is a function `f : G → ℝ` that sends one to zero, is submultiplicative and such that `f x⁻¹ = f x` and `f x = 0 → x = 1` for all `x`.

- toFun : G → ℝ
- map_one' : self.toFun 1 = 0
- mul_le' (x y : G) : self.toFun (x * y) ≤ self.toFun x + self.toFun y
- inv' (x : G) : self.toFun x⁻¹ = self.toFun x
- eq_one_of_map_eq_zero' (x : G) : self.toFun x = 0 → x = 1

  If the image under the norm is zero, then the argument is one.

Instances For

source
structure NonarchAddGroupNorm (G : Type u_6) [AddGroup G] extends NonarchAddGroupSeminorm G :
Type u_6

A nonarchimedean norm on an additive group `G` is a function `f : G → ℝ` that preserves zero, is nonarchimedean and such that `f (-x) = f x` and `f x = 0 → x = 0` for all `x`.

- toFun : G → ℝ
- map_zero' : self.toFun 0 = 0
- add_le_max' (r s : G) : self.toFun (r + s) ≤ max (self.toFun r) (self.toFun s)
- neg' (r : G) : self.toFun (-r) = self.toFun r
- eq_zero_of_map_eq_zero' (x : G) : self.toFun x = 0 → x = 0

  If the image under the norm is zero, then the argument is zero.

Instances For

source
class NonarchAddGroupSeminormClass (F : Type u_6) (α : outParam (Type u_7)) [AddGroup α] [FunLike F α ℝ] extends NonarchimedeanHomClass F α ℝ :
Prop

`NonarchAddGroupSeminormClass F α` states that `F` is a type of nonarchimedean seminorms on the additive group `α`.

You should extend this class when you extend `NonarchAddGroupSeminorm`.

- map_add_le_max (f : F) (a b : α) : f (a + b) ≤ max (f a) (f b)
- map_zero (f : F) : f 0 = 0

  The image of zero is zero.

- map_neg_eq_map' (f : F) (a : α) : f (-a) = f a

  The seminorm is invariant under negation.

Instances

source
class NonarchAddGroupNormClass (F : Type u_6) (α : outParam (Type u_7)) [AddGroup α] [FunLike F α ℝ] extends NonarchAddGroupSeminormClass F α :
Prop

`NonarchAddGroupNormClass F α` states that `F` is a type of nonarchimedean norms on the additive group `α`.

You should extend this class when you extend `NonarchAddGroupNorm`.

- map_add_le_max (f : F) (a b : α) : f (a + b) ≤ max (f a) (f b)
- map_zero (f : F) : f 0 = 0
- map_neg_eq_map' (f : F) (a : α) : f (-a) = f a
- eq_zero_of_map_eq_zero (f : F) {a : α} : f a = 0 → a = 0

  If the image under the norm is zero, then the argument is zero.

Instances

source
theorem map_sub_le_max {E : Type u_3} {F : Type u_4} [AddGroup E] [FunLike F E ℝ] [NonarchAddGroupSeminormClass F E] (f : F) (x y : E) :
f (x - y) ≤ max (f x) (f y)
source
@[instance 100]
instance NonarchAddGroupSeminormClass.toAddGroupSeminormClass {E : Type u_3} {F : Type u_4} [FunLike F E ℝ] [AddGroup E] [NonarchAddGroupSeminormClass F E] :
AddGroupSeminormClass F E ℝ
source
@[instance 100]
instance NonarchAddGroupNormClass.toAddGroupNormClass {E : Type u_3} {F : Type u_4} [FunLike F E ℝ] [AddGroup E] [NonarchAddGroupNormClass F E] :
AddGroupNormClass F E ℝ

### Seminorms #

source
instance GroupSeminorm.funLike {E : Type u_3} [Group E] :
FunLike (GroupSeminorm E) E ℝ
Equations

- GroupSeminorm.funLike = { coe := fun (f : GroupSeminorm E) => f.toFun, coe_injective' := ⋯ }

source
instance AddGroupSeminorm.funLike {E : Type u_3} [AddGroup E] :
FunLike (AddGroupSeminorm E) E ℝ
Equations

- AddGroupSeminorm.funLike = { coe := fun (f : AddGroupSeminorm E) => f.toFun, coe_injective' := ⋯ }

source
instance GroupSeminorm.groupSeminormClass {E : Type u_3} [Group E] :
GroupSeminormClass (GroupSeminorm E) E ℝ
source
instance AddGroupSeminorm.addGroupSeminormClass {E : Type u_3} [AddGroup E] :
AddGroupSeminormClass (AddGroupSeminorm E) E ℝ
source
@[simp]
theorem GroupSeminorm.toFun_eq_coe {E : Type u_3} [Group E] {p : GroupSeminorm E} :
p.toFun = ⇑p
source
@[simp]
theorem AddGroupSeminorm.toFun_eq_coe {E : Type u_3} [AddGroup E] {p : AddGroupSeminorm E} :
p.toFun = ⇑p
source
theorem GroupSeminorm.ext {E : Type u_3} [Group E] {p q : GroupSeminorm E} :
(∀ (x : E), p x = q x) → p = q
source
theorem AddGroupSeminorm.ext {E : Type u_3} [AddGroup E] {p q : AddGroupSeminorm E} :
(∀ (x : E), p x = q x) → p = q
source
theorem AddGroupSeminorm.ext_iff {E : Type u_3} [AddGroup E] {p q : AddGroupSeminorm E} :
p = q ↔ ∀ (x : E), p x = q x
source
theorem GroupSeminorm.ext_iff {E : Type u_3} [Group E] {p q : GroupSeminorm E} :
p = q ↔ ∀ (x : E), p x = q x
source
instance GroupSeminorm.instPartialOrder {E : Type u_3} [Group E] :
PartialOrder (GroupSeminorm E)
Equations

- GroupSeminorm.instPartialOrder = PartialOrder.lift (fun (f : GroupSeminorm E) => ⇑f) ⋯

source
instance AddGroupSeminorm.instPartialOrder {E : Type u_3} [AddGroup E] :
PartialOrder (AddGroupSeminorm E)
Equations

- AddGroupSeminorm.instPartialOrder = PartialOrder.lift (fun (f : AddGroupSeminorm E) => ⇑f) ⋯

source
theorem GroupSeminorm.le_def {E : Type u_3} [Group E] {p q : GroupSeminorm E} :
p ≤ q ↔ ⇑p ≤ ⇑q
source
theorem AddGroupSeminorm.le_def {E : Type u_3} [AddGroup E] {p q : AddGroupSeminorm E} :
p ≤ q ↔ ⇑p ≤ ⇑q
source
theorem GroupSeminorm.lt_def {E : Type u_3} [Group E] {p q : GroupSeminorm E} :
p < q ↔ ⇑p < ⇑q
source
theorem AddGroupSeminorm.lt_def {E : Type u_3} [AddGroup E] {p q : AddGroupSeminorm E} :
p < q ↔ ⇑p < ⇑q
source
@[simp]
theorem GroupSeminorm.coe_le_coe {E : Type u_3} [Group E] {p q : GroupSeminorm E} :
⇑p ≤ ⇑q ↔ p ≤ q
source
@[simp]
theorem AddGroupSeminorm.coe_le_coe {E : Type u_3} [AddGroup E] {p q : AddGroupSeminorm E} :
⇑p ≤ ⇑q ↔ p ≤ q
source
@[simp]
theorem GroupSeminorm.coe_lt_coe {E : Type u_3} [Group E] {p q : GroupSeminorm E} :
⇑p < ⇑q ↔ p < q
source
@[simp]
theorem AddGroupSeminorm.coe_lt_coe {E : Type u_3} [AddGroup E] {p q : AddGroupSeminorm E} :
⇑p < ⇑q ↔ p < q
source
instance GroupSeminorm.instZeroGroupSeminorm {E : Type u_3} [Group E] :
Zero (GroupSeminorm E)
Equations

- GroupSeminorm.instZeroGroupSeminorm = { zero := { toFun := 0, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }

source
instance AddGroupSeminorm.instZeroAddGroupSeminorm {E : Type u_3} [AddGroup E] :
Zero (AddGroupSeminorm E)
Equations

- AddGroupSeminorm.instZeroAddGroupSeminorm = { zero := { toFun := 0, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }

source
@[simp]
theorem GroupSeminorm.coe_zero {E : Type u_3} [Group E] :
⇑0 = 0
source
@[simp]
theorem AddGroupSeminorm.coe_zero {E : Type u_3} [AddGroup E] :
⇑0 = 0
source
@[simp]
theorem GroupSeminorm.zero_apply {E : Type u_3} [Group E] (x : E) :
0 x = 0
source
@[simp]
theorem AddGroupSeminorm.zero_apply {E : Type u_3} [AddGroup E] (x : E) :
0 x = 0
source
instance GroupSeminorm.instInhabited {E : Type u_3} [Group E] :
Inhabited (GroupSeminorm E)
Equations

- GroupSeminorm.instInhabited = { default := 0 }

source
instance AddGroupSeminorm.instInhabited {E : Type u_3} [AddGroup E] :
Inhabited (AddGroupSeminorm E)
Equations

- AddGroupSeminorm.instInhabited = { default := 0 }

source
instance GroupSeminorm.instAdd {E : Type u_3} [Group E] :
Add (GroupSeminorm E)
Equations

- GroupSeminorm.instAdd = { add := fun (p q : GroupSeminorm E) => { toFun := fun (x : E) => p x + q x, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }

source
instance AddGroupSeminorm.instAdd {E : Type u_3} [AddGroup E] :
Add (AddGroupSeminorm E)
Equations

- AddGroupSeminorm.instAdd = { add := fun (p q : AddGroupSeminorm E) => { toFun := fun (x : E) => p x + q x, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }

source
@[simp]
theorem GroupSeminorm.coe_add {E : Type u_3} [Group E] (p q : GroupSeminorm E) :
⇑(p + q) = ⇑p + ⇑q
source
@[simp]
theorem AddGroupSeminorm.coe_add {E : Type u_3} [AddGroup E] (p q : AddGroupSeminorm E) :
⇑(p + q) = ⇑p + ⇑q
source
@[simp]
theorem GroupSeminorm.add_apply {E : Type u_3} [Group E] (p q : GroupSeminorm E) (x : E) :
(p + q) x = p x + q x
source
@[simp]
theorem AddGroupSeminorm.add_apply {E : Type u_3} [AddGroup E] (p q : AddGroupSeminorm E) (x : E) :
(p + q) x = p x + q x
source
instance GroupSeminorm.instMax {E : Type u_3} [Group E] :
Max (GroupSeminorm E)
Equations

- GroupSeminorm.instMax = { max := fun (p q : GroupSeminorm E) => { toFun := ⇑p ⊔ ⇑q, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }

source
instance AddGroupSeminorm.instMax {E : Type u_3} [AddGroup E] :
Max (AddGroupSeminorm E)
Equations

- AddGroupSeminorm.instMax = { max := fun (p q : AddGroupSeminorm E) => { toFun := ⇑p ⊔ ⇑q, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }

source
@[simp]
theorem GroupSeminorm.coe_sup {E : Type u_3} [Group E] (p q : GroupSeminorm E) :
⇑(p ⊔ q) = ⇑p ⊔ ⇑q
source
@[simp]
theorem AddGroupSeminorm.coe_sup {E : Type u_3} [AddGroup E] (p q : AddGroupSeminorm E) :
⇑(p ⊔ q) = ⇑p ⊔ ⇑q
source
@[simp]
theorem GroupSeminorm.sup_apply {E : Type u_3} [Group E] (p q : GroupSeminorm E) (x : E) :
(p ⊔ q) x = max (p x) (q x)
source
@[simp]
theorem AddGroupSeminorm.sup_apply {E : Type u_3} [AddGroup E] (p q : AddGroupSeminorm E) (x : E) :
(p ⊔ q) x = max (p x) (q x)
source
instance GroupSeminorm.semilatticeSup {E : Type u_3} [Group E] :
SemilatticeSup (GroupSeminorm E)
Equations

- GroupSeminorm.semilatticeSup = Function.Injective.semilatticeSup (fun (f : GroupSeminorm E) => ⇑f) ⋯ ⋯

source
instance AddGroupSeminorm.semilatticeSup {E : Type u_3} [AddGroup E] :
SemilatticeSup (AddGroupSeminorm E)
Equations

- AddGroupSeminorm.semilatticeSup = Function.Injective.semilatticeSup (fun (f : AddGroupSeminorm E) => ⇑f) ⋯ ⋯

source
def GroupSeminorm.comp {E : Type u_3} {F : Type u_4} [Group E] [Group F] (p : GroupSeminorm E) (f : F →* E) :
GroupSeminorm F

Composition of a group seminorm with a monoid homomorphism as a group seminorm.

Equations

- p.comp f = { toFun := fun (x : F) => p (f x), map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ }

Instances For

source
def AddGroupSeminorm.comp {E : Type u_3} {F : Type u_4} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) (f : F →+ E) :
AddGroupSeminorm F

Composition of an additive group seminorm with an additive monoid homomorphism as an additive group seminorm.

Equations

- p.comp f = { toFun := fun (x : F) => p (f x), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ }

Instances For

source
@[simp]
theorem GroupSeminorm.coe_comp {E : Type u_3} {F : Type u_4} [Group E] [Group F] (p : GroupSeminorm E) (f : F →* E) :
⇑(p.comp f) = ⇑p ∘ ⇑f
source
@[simp]
theorem AddGroupSeminorm.coe_comp {E : Type u_3} {F : Type u_4} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) (f : F →+ E) :
⇑(p.comp f) = ⇑p ∘ ⇑f
source
@[simp]
theorem GroupSeminorm.comp_apply {E : Type u_3} {F : Type u_4} [Group E] [Group F] (p : GroupSeminorm E) (f : F →* E) (x : F) :
(p.comp f) x = p (f x)
source
@[simp]
theorem AddGroupSeminorm.comp_apply {E : Type u_3} {F : Type u_4} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) (f : F →+ E) (x : F) :
(p.comp f) x = p (f x)
source
@[simp]
theorem GroupSeminorm.comp_id {E : Type u_3} [Group E] (p : GroupSeminorm E) :
p.comp (MonoidHom.id E) = p
source
@[simp]
theorem AddGroupSeminorm.comp_id {E : Type u_3} [AddGroup E] (p : AddGroupSeminorm E) :
p.comp (AddMonoidHom.id E) = p
source
@[simp]
theorem GroupSeminorm.comp_zero {E : Type u_3} {F : Type u_4} [Group E] [Group F] (p : GroupSeminorm E) :
p.comp 1 = 0
source
@[simp]
theorem AddGroupSeminorm.comp_zero {E : Type u_3} {F : Type u_4} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) :
p.comp 0 = 0
source
@[simp]
theorem GroupSeminorm.zero_comp {E : Type u_3} {F : Type u_4} [Group E] [Group F] (f : F →* E) :
comp 0 f = 0
source
@[simp]
theorem AddGroupSeminorm.zero_comp {E : Type u_3} {F : Type u_4} [AddGroup E] [AddGroup F] (f : F →+ E) :
comp 0 f = 0
source
theorem GroupSeminorm.comp_assoc {E : Type u_3} {F : Type u_4} {G : Type u_5} [Group E] [Group F] [Group G] (p : GroupSeminorm E) (g : F →* E) (f : G →* F) :
p.comp (g.comp f) = (p.comp g).comp f
source
theorem AddGroupSeminorm.comp_assoc {E : Type u_3} {F : Type u_4} {G : Type u_5} [AddGroup E] [AddGroup F] [AddGroup G] (p : AddGroupSeminorm E) (g : F →+ E) (f : G →+ F) :
p.comp (g.comp f) = (p.comp g).comp f
source
theorem GroupSeminorm.add_comp {E : Type u_3} {F : Type u_4} [Group E] [Group F] (p q : GroupSeminorm E) (f : F →* E) :
(p + q).comp f = p.comp f + q.comp f
source
theorem AddGroupSeminorm.add_comp {E : Type u_3} {F : Type u_4} [AddGroup E] [AddGroup F] (p q : AddGroupSeminorm E) (f : F →+ E) :
(p + q).comp f = p.comp f + q.comp f
source
theorem GroupSeminorm.comp_mono {E : Type u_3} {F : Type u_4} [Group E] [Group F] {p q : GroupSeminorm E} (f : F →* E) (hp : p ≤ q) :
p.comp f ≤ q.comp f
source
theorem AddGroupSeminorm.comp_mono {E : Type u_3} {F : Type u_4} [AddGroup E] [AddGroup F] {p q : AddGroupSeminorm E} (f : F →+ E) (hp : p ≤ q) :
p.comp f ≤ q.comp f
source
theorem GroupSeminorm.comp_mul_le {E : Type u_3} {F : Type u_4} [CommGroup E] [CommGroup F] (p : GroupSeminorm E) (f g : F →* E) :
p.comp (f * g) ≤ p.comp f + p.comp g
source
theorem AddGroupSeminorm.comp_add_le {E : Type u_3} {F : Type u_4} [AddCommGroup E] [AddCommGroup F] (p : AddGroupSeminorm E) (f g : F →+ E) :
p.comp (f + g) ≤ p.comp f + p.comp g
source
theorem GroupSeminorm.mul_bddBelow_range_add {E : Type u_3} [CommGroup E] {p q : GroupSeminorm E} {x : E} :
BddBelow (Set.range fun (y : E) => p y + q (x / y))
source
theorem AddGroupSeminorm.add_bddBelow_range_add {E : Type u_3} [AddCommGroup E] {p q : AddGroupSeminorm E} {x : E} :
BddBelow (Set.range fun (y : E) => p y + q (x - y))
source
noncomputable instance GroupSeminorm.instMin {E : Type u_3} [CommGroup E] :
Min (GroupSeminorm E)
Equations

- GroupSeminorm.instMin = { min := fun (p q : GroupSeminorm E) => { toFun := fun (x : E) => ⨅ (y : E), p y + q (x / y), map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }

source
noncomputable instance AddGroupSeminorm.instMin {E : Type u_3} [AddCommGroup E] :
Min (AddGroupSeminorm E)
Equations

- AddGroupSeminorm.instMin = { min := fun (p q : AddGroupSeminorm E) => { toFun := fun (x : E) => ⨅ (y : E), p y + q (x - y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }

source
@[simp]
theorem GroupSeminorm.inf_apply {E : Type u_3} [CommGroup E] (p q : GroupSeminorm E) (x : E) :
(p ⊓ q) x = ⨅ (y : E), p y + q (x / y)
source
@[simp]
theorem AddGroupSeminorm.inf_apply {E : Type u_3} [AddCommGroup E] (p q : AddGroupSeminorm E) (x : E) :
(p ⊓ q) x = ⨅ (y : E), p y + q (x - y)
source
noncomputable instance GroupSeminorm.instLattice {E : Type u_3} [CommGroup E] :
Lattice (GroupSeminorm E)
Equations

- GroupSeminorm.instLattice = { toSemilatticeSup := GroupSeminorm.semilatticeSup, inf := fun (x1 x2 : GroupSeminorm E) => x1 ⊓ x2, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

source
noncomputable instance AddGroupSeminorm.instLattice {E : Type u_3} [AddCommGroup E] :
Lattice (AddGroupSeminorm E)
Equations

- AddGroupSeminorm.instLattice = { toSemilatticeSup := AddGroupSeminorm.semilatticeSup, inf := fun (x1 x2 : AddGroupSeminorm E) => x1 ⊓ x2, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

source
instance AddGroupSeminorm.toOne {E : Type u_3} [AddGroup E] [DecidableEq E] :
One (AddGroupSeminorm E)
Equations

- AddGroupSeminorm.toOne = { one := { toFun := fun (x : E) => if x = 0 then 0 else 1, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }

source
@[simp]
theorem AddGroupSeminorm.apply_one {E : Type u_3} [AddGroup E] [DecidableEq E] (x : E) :
1 x = if x = 0 then 0 else 1
source
instance AddGroupSeminorm.toSMul {R : Type u_1} {E : Type u_3} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] :
SMul R (AddGroupSeminorm E)

Any action on `ℝ` which factors through `ℝ≥0` applies to an `AddGroupSeminorm`.

Equations

- AddGroupSeminorm.toSMul = { smul := fun (r : R) (p : AddGroupSeminorm E) => { toFun := fun (x : E) => r • p x, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }

source
@[simp]
theorem AddGroupSeminorm.coe_smul {R : Type u_1} {E : Type u_3} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : AddGroupSeminorm E) :
⇑(r • p) = r • ⇑p
source
@[simp]
theorem AddGroupSeminorm.smul_apply {R : Type u_1} {E : Type u_3} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : AddGroupSeminorm E) (x : E) :
(r • p) x = r • p x
source
instance AddGroupSeminorm.isScalarTower {R : Type u_1} {R' : Type u_2} {E : Type u_3} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] [SMul R' ℝ] [SMul R' NNReal] [IsScalarTower R' NNReal ℝ] [SMul R R'] [IsScalarTower R R' ℝ] :
IsScalarTower R R' (AddGroupSeminorm E)
source
theorem AddGroupSeminorm.smul_sup {R : Type u_1} {E : Type u_3} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p q : AddGroupSeminorm E) :
r • (p ⊔ q) = r • p ⊔ r • q
source
instance NonarchAddGroupSeminorm.funLike {E : Type u_3} [AddGroup E] :
FunLike (NonarchAddGroupSeminorm E) E ℝ
Equations

- NonarchAddGroupSeminorm.funLike = { coe := fun (f : NonarchAddGroupSeminorm E) => f.toFun, coe_injective' := ⋯ }

source
instance NonarchAddGroupSeminorm.nonarchAddGroupSeminormClass {E : Type u_3} [AddGroup E] :
NonarchAddGroupSeminormClass (NonarchAddGroupSeminorm E) E
source
@[simp]
theorem NonarchAddGroupSeminorm.toZeroHom_eq_coe {E : Type u_3} [AddGroup E] {p : NonarchAddGroupSeminorm E} :
⇑p.toZeroHom = ⇑p
source
theorem NonarchAddGroupSeminorm.ext {E : Type u_3} [AddGroup E] {p q : NonarchAddGroupSeminorm E} :
(∀ (x : E), p x = q x) → p = q
source
theorem NonarchAddGroupSeminorm.ext_iff {E : Type u_3} [AddGroup E] {p q : NonarchAddGroupSeminorm E} :
p = q ↔ ∀ (x : E), p x = q x
source
noncomputable instance NonarchAddGroupSeminorm.instPartialOrder {E : Type u_3} [AddGroup E] :
PartialOrder (NonarchAddGroupSeminorm E)
Equations

- NonarchAddGroupSeminorm.instPartialOrder = PartialOrder.lift (fun (f : NonarchAddGroupSeminorm E) => ⇑f) ⋯

source
theorem NonarchAddGroupSeminorm.le_def {E : Type u_3} [AddGroup E] {p q : NonarchAddGroupSeminorm E} :
p ≤ q ↔ ⇑p ≤ ⇑q
source
theorem NonarchAddGroupSeminorm.lt_def {E : Type u_3} [AddGroup E] {p q : NonarchAddGroupSeminorm E} :
p < q ↔ ⇑p < ⇑q
source
@[simp]
theorem NonarchAddGroupSeminorm.coe_le_coe {E : Type u_3} [AddGroup E] {p q : NonarchAddGroupSeminorm E} :
⇑p ≤ ⇑q ↔ p ≤ q
source
@[simp]
theorem NonarchAddGroupSeminorm.coe_lt_coe {E : Type u_3} [AddGroup E] {p q : NonarchAddGroupSeminorm E} :
⇑p < ⇑q ↔ p < q
source
instance NonarchAddGroupSeminorm.instZero {E : Type u_3} [AddGroup E] :
Zero (NonarchAddGroupSeminorm E)
Equations

- NonarchAddGroupSeminorm.instZero = { zero := { toFun := 0, map_zero' := ⋯, add_le_max' := ⋯, neg' := ⋯ } }

source
@[simp]
theorem NonarchAddGroupSeminorm.coe_zero {E : Type u_3} [AddGroup E] :
⇑0 = 0
source
@[simp]
theorem NonarchAddGroupSeminorm.zero_apply {E : Type u_3} [AddGroup E] (x : E) :
0 x = 0
source
instance NonarchAddGroupSeminorm.instInhabited {E : Type u_3} [AddGroup E] :
Inhabited (NonarchAddGroupSeminorm E)
Equations

- NonarchAddGroupSeminorm.instInhabited = { default := 0 }

source
instance NonarchAddGroupSeminorm.instMax {E : Type u_3} [AddGroup E] :
Max (NonarchAddGroupSeminorm E)
Equations

- NonarchAddGroupSeminorm.instMax = { max := fun (p q : NonarchAddGroupSeminorm E) => { toFun := ⇑p ⊔ ⇑q, map_zero' := ⋯, add_le_max' := ⋯, neg' := ⋯ } }

source
@[simp]
theorem NonarchAddGroupSeminorm.coe_sup {E : Type u_3} [AddGroup E] (p q : NonarchAddGroupSeminorm E) :
⇑(p ⊔ q) = ⇑p ⊔ ⇑q
source
@[simp]
theorem NonarchAddGroupSeminorm.sup_apply {E : Type u_3} [AddGroup E] (p q : NonarchAddGroupSeminorm E) (x : E) :
(p ⊔ q) x = max (p x) (q x)
source
noncomputable instance NonarchAddGroupSeminorm.instSemilatticeSup {E : Type u_3} [AddGroup E] :
SemilatticeSup (NonarchAddGroupSeminorm E)
Equations

- NonarchAddGroupSeminorm.instSemilatticeSup = Function.Injective.semilatticeSup (fun (f : NonarchAddGroupSeminorm E) => ⇑f) ⋯ ⋯

source
theorem NonarchAddGroupSeminorm.add_bddBelow_range_add {E : Type u_3} [AddCommGroup E] {p q : NonarchAddGroupSeminorm E} {x : E} :
BddBelow (Set.range fun (y : E) => p y + q (x - y))
source
instance GroupSeminorm.toOne {E : Type u_3} [Group E] [DecidableEq E] :
One (GroupSeminorm E)
Equations

- GroupSeminorm.toOne = { one := { toFun := fun (x : E) => if x = 1 then 0 else 1, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }

source
@[simp]
theorem GroupSeminorm.apply_one {E : Type u_3} [Group E] [DecidableEq E] (x : E) :
1 x = if x = 1 then 0 else 1
source
instance GroupSeminorm.instSMul {R : Type u_1} {E : Type u_3} [Group E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] :
SMul R (GroupSeminorm E)

Any action on `ℝ` which factors through `ℝ≥0` applies to an `AddGroupSeminorm`.

Equations

- GroupSeminorm.instSMul = { smul := fun (r : R) (p : GroupSeminorm E) => { toFun := fun (x : E) => r • p x, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }

source
instance GroupSeminorm.instIsScalarTowerOfReal {R : Type u_1} {R' : Type u_2} {E : Type u_3} [Group E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] [SMul R' ℝ] [SMul R' NNReal] [IsScalarTower R' NNReal ℝ] [SMul R R'] [IsScalarTower R R' ℝ] :
IsScalarTower R R' (GroupSeminorm E)
source
@[simp]
theorem GroupSeminorm.coe_smul {R : Type u_1} {E : Type u_3} [Group E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : GroupSeminorm E) :
⇑(r • p) = r • ⇑p
source
@[simp]
theorem GroupSeminorm.smul_apply {R : Type u_1} {E : Type u_3} [Group E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : GroupSeminorm E) (x : E) :
(r • p) x = r • p x
source
theorem GroupSeminorm.smul_sup {R : Type u_1} {E : Type u_3} [Group E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p q : GroupSeminorm E) :
r • (p ⊔ q) = r • p ⊔ r • q
source
instance NonarchAddGroupSeminorm.instOneOfDecidableEq {E : Type u_3} [AddGroup E] [DecidableEq E] :
One (NonarchAddGroupSeminorm E)
Equations

- NonarchAddGroupSeminorm.instOneOfDecidableEq = { one := { toFun := fun (x : E) => if x = 0 then 0 else 1, map_zero' := ⋯, add_le_max' := ⋯, neg' := ⋯ } }

source
@[simp]
theorem NonarchAddGroupSeminorm.apply_one {E : Type u_3} [AddGroup E] [DecidableEq E] (x : E) :
1 x = if x = 0 then 0 else 1
source
instance NonarchAddGroupSeminorm.instSMul {R : Type u_1} {E : Type u_3} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] :
SMul R (NonarchAddGroupSeminorm E)

Any action on `ℝ` which factors through `ℝ≥0` applies to a `NonarchAddGroupSeminorm`.

Equations

- NonarchAddGroupSeminorm.instSMul = { smul := fun (r : R) (p : NonarchAddGroupSeminorm E) => { toFun := fun (x : E) => r • p x, map_zero' := ⋯, add_le_max' := ⋯, neg' := ⋯ } }

source
instance NonarchAddGroupSeminorm.instIsScalarTowerOfReal {R : Type u_1} {R' : Type u_2} {E : Type u_3} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] [SMul R' ℝ] [SMul R' NNReal] [IsScalarTower R' NNReal ℝ] [SMul R R'] [IsScalarTower R R' ℝ] :
IsScalarTower R R' (NonarchAddGroupSeminorm E)
source
@[simp]
theorem NonarchAddGroupSeminorm.coe_smul {R : Type u_1} {E : Type u_3} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : NonarchAddGroupSeminorm E) :
⇑(r • p) = r • ⇑p
source
@[simp]
theorem NonarchAddGroupSeminorm.smul_apply {R : Type u_1} {E : Type u_3} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : NonarchAddGroupSeminorm E) (x : E) :
(r • p) x = r • p x
source
theorem NonarchAddGroupSeminorm.smul_sup {R : Type u_1} {E : Type u_3} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p q : NonarchAddGroupSeminorm E) :
r • (p ⊔ q) = r • p ⊔ r • q

### Norms #

source
instance GroupNorm.funLike {E : Type u_3} [Group E] :
FunLike (GroupNorm E) E ℝ
Equations

- GroupNorm.funLike = { coe := fun (f : GroupNorm E) => f.toFun, coe_injective' := ⋯ }

source
instance AddGroupNorm.funLike {E : Type u_3} [AddGroup E] :
FunLike (AddGroupNorm E) E ℝ
Equations

- AddGroupNorm.funLike = { coe := fun (f : AddGroupNorm E) => f.toFun, coe_injective' := ⋯ }

source
instance GroupNorm.groupNormClass {E : Type u_3} [Group E] :
GroupNormClass (GroupNorm E) E ℝ
source
instance AddGroupNorm.addGroupNormClass {E : Type u_3} [AddGroup E] :
AddGroupNormClass (AddGroupNorm E) E ℝ
source
@[simp]
theorem GroupNorm.toGroupSeminorm_eq_coe {E : Type u_3} [Group E] {p : GroupNorm E} :
⇑p.toGroupSeminorm = ⇑p
source
@[simp]
theorem AddGroupNorm.toAddGroupSeminorm_eq_coe {E : Type u_3} [AddGroup E] {p : AddGroupNorm E} :
⇑p.toAddGroupSeminorm = ⇑p
source
theorem GroupNorm.ext {E : Type u_3} [Group E] {p q : GroupNorm E} :
(∀ (x : E), p x = q x) → p = q
source
theorem AddGroupNorm.ext {E : Type u_3} [AddGroup E] {p q : AddGroupNorm E} :
(∀ (x : E), p x = q x) → p = q
source
theorem GroupNorm.ext_iff {E : Type u_3} [Group E] {p q : GroupNorm E} :
p = q ↔ ∀ (x : E), p x = q x
source
theorem AddGroupNorm.ext_iff {E : Type u_3} [AddGroup E] {p q : AddGroupNorm E} :
p = q ↔ ∀ (x : E), p x = q x
source
instance GroupNorm.instPartialOrder {E : Type u_3} [Group E] :
PartialOrder (GroupNorm E)
Equations

- GroupNorm.instPartialOrder = PartialOrder.lift (fun (f : GroupNorm E) => ⇑f) ⋯

source
instance AddGroupNorm.instPartialOrder {E : Type u_3} [AddGroup E] :
PartialOrder (AddGroupNorm E)
Equations

- AddGroupNorm.instPartialOrder = PartialOrder.lift (fun (f : AddGroupNorm E) => ⇑f) ⋯

source
theorem GroupNorm.le_def {E : Type u_3} [Group E] {p q : GroupNorm E} :
p ≤ q ↔ ⇑p ≤ ⇑q
source
theorem AddGroupNorm.le_def {E : Type u_3} [AddGroup E] {p q : AddGroupNorm E} :
p ≤ q ↔ ⇑p ≤ ⇑q
source
theorem GroupNorm.lt_def {E : Type u_3} [Group E] {p q : GroupNorm E} :
p < q ↔ ⇑p < ⇑q
source
theorem AddGroupNorm.lt_def {E : Type u_3} [AddGroup E] {p q : AddGroupNorm E} :
p < q ↔ ⇑p < ⇑q
source
@[simp]
theorem GroupNorm.coe_le_coe {E : Type u_3} [Group E] {p q : GroupNorm E} :
⇑p ≤ ⇑q ↔ p ≤ q
source
@[simp]
theorem AddGroupNorm.coe_le_coe {E : Type u_3} [AddGroup E] {p q : AddGroupNorm E} :
⇑p ≤ ⇑q ↔ p ≤ q
source
@[simp]
theorem GroupNorm.coe_lt_coe {E : Type u_3} [Group E] {p q : GroupNorm E} :
⇑p < ⇑q ↔ p < q
source
@[simp]
theorem AddGroupNorm.coe_lt_coe {E : Type u_3} [AddGroup E] {p q : AddGroupNorm E} :
⇑p < ⇑q ↔ p < q
source
instance GroupNorm.instAdd {E : Type u_3} [Group E] :
Add (GroupNorm E)
Equations

- GroupNorm.instAdd = { add := fun (p q : GroupNorm E) => let __src := p.toGroupSeminorm + q.toGroupSeminorm; { toGroupSeminorm := __src, eq_one_of_map_eq_zero' := ⋯ } }

source
instance AddGroupNorm.instAdd {E : Type u_3} [AddGroup E] :
Add (AddGroupNorm E)
Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem GroupNorm.coe_add {E : Type u_3} [Group E] (p q : GroupNorm E) :
⇑(p + q) = ⇑p + ⇑q
source
@[simp]
theorem AddGroupNorm.coe_add {E : Type u_3} [AddGroup E] (p q : AddGroupNorm E) :
⇑(p + q) = ⇑p + ⇑q
source
@[simp]
theorem GroupNorm.add_apply {E : Type u_3} [Group E] (p q : GroupNorm E) (x : E) :
(p + q) x = p x + q x
source
@[simp]
theorem AddGroupNorm.add_apply {E : Type u_3} [AddGroup E] (p q : AddGroupNorm E) (x : E) :
(p + q) x = p x + q x
source
instance GroupNorm.instMax {E : Type u_3} [Group E] :
Max (GroupNorm E)
Equations

- GroupNorm.instMax = { max := fun (p q : GroupNorm E) => let __src := p.toGroupSeminorm ⊔ q.toGroupSeminorm; { toGroupSeminorm := __src, eq_one_of_map_eq_zero' := ⋯ } }

source
instance AddGroupNorm.instMax {E : Type u_3} [AddGroup E] :
Max (AddGroupNorm E)
Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem GroupNorm.coe_sup {E : Type u_3} [Group E] (p q : GroupNorm E) :
⇑(p ⊔ q) = ⇑p ⊔ ⇑q
source
@[simp]
theorem AddGroupNorm.coe_sup {E : Type u_3} [AddGroup E] (p q : AddGroupNorm E) :
⇑(p ⊔ q) = ⇑p ⊔ ⇑q
source
@[simp]
theorem GroupNorm.sup_apply {E : Type u_3} [Group E] (p q : GroupNorm E) (x : E) :
(p ⊔ q) x = max (p x) (q x)
source
@[simp]
theorem AddGroupNorm.sup_apply {E : Type u_3} [AddGroup E] (p q : AddGroupNorm E) (x : E) :
(p ⊔ q) x = max (p x) (q x)
source
instance GroupNorm.instSemilatticeSup {E : Type u_3} [Group E] :
SemilatticeSup (GroupNorm E)
Equations

- GroupNorm.instSemilatticeSup = Function.Injective.semilatticeSup (fun (f : GroupNorm E) => ⇑f) ⋯ ⋯

source
instance AddGroupNorm.instSemilatticeSup {E : Type u_3} [AddGroup E] :
SemilatticeSup (AddGroupNorm E)
Equations

- AddGroupNorm.instSemilatticeSup = Function.Injective.semilatticeSup (fun (f : AddGroupNorm E) => ⇑f) ⋯ ⋯

source
instance AddGroupNorm.instOne {E : Type u_3} [AddGroup E] [DecidableEq E] :
One (AddGroupNorm E)
Equations

- AddGroupNorm.instOne = { one := let __src := 1; { toAddGroupSeminorm := __src, eq_zero_of_map_eq_zero' := ⋯ } }

source
@[simp]
theorem AddGroupNorm.apply_one {E : Type u_3} [AddGroup E] [DecidableEq E] (x : E) :
1 x = if x = 0 then 0 else 1
source
instance AddGroupNorm.instInhabited {E : Type u_3} [AddGroup E] [DecidableEq E] :
Inhabited (AddGroupNorm E)
Equations

- AddGroupNorm.instInhabited = { default := 1 }

source
instance AddGroupNorm.toOne {E : Type u_3} [AddGroup E] [DecidableEq E] :
One (AddGroupNorm E)
Equations

- AddGroupNorm.toOne = { one := let __src := 1; { toAddGroupSeminorm := __src, eq_zero_of_map_eq_zero' := ⋯ } }

source
instance GroupNorm.toOne {E : Type u_3} [Group E] [DecidableEq E] :
One (GroupNorm E)
Equations

- GroupNorm.toOne = { one := let __src := 1; { toGroupSeminorm := __src, eq_one_of_map_eq_zero' := ⋯ } }

source
@[simp]
theorem GroupNorm.apply_one {E : Type u_3} [Group E] [DecidableEq E] (x : E) :
1 x = if x = 1 then 0 else 1
source
instance GroupNorm.instInhabited {E : Type u_3} [Group E] [DecidableEq E] :
Inhabited (GroupNorm E)
Equations

- GroupNorm.instInhabited = { default := 1 }

source
instance NonarchAddGroupNorm.funLike {E : Type u_3} [AddGroup E] :
FunLike (NonarchAddGroupNorm E) E ℝ
Equations

- NonarchAddGroupNorm.funLike = { coe := fun (f : NonarchAddGroupNorm E) => f.toFun, coe_injective' := ⋯ }

source
instance NonarchAddGroupNorm.nonarchAddGroupNormClass {E : Type u_3} [AddGroup E] :
NonarchAddGroupNormClass (NonarchAddGroupNorm E) E
source
@[simp]
theorem NonarchAddGroupNorm.toNonarchAddGroupSeminorm_eq_coe {E : Type u_3} [AddGroup E] {p : NonarchAddGroupNorm E} :
⇑p.toNonarchAddGroupSeminorm = ⇑p
source
theorem NonarchAddGroupNorm.ext {E : Type u_3} [AddGroup E] {p q : NonarchAddGroupNorm E} :
(∀ (x : E), p x = q x) → p = q
source
theorem NonarchAddGroupNorm.ext_iff {E : Type u_3} [AddGroup E] {p q : NonarchAddGroupNorm E} :
p = q ↔ ∀ (x : E), p x = q x
source
noncomputable instance NonarchAddGroupNorm.instPartialOrder {E : Type u_3} [AddGroup E] :
PartialOrder (NonarchAddGroupNorm E)
Equations

- NonarchAddGroupNorm.instPartialOrder = PartialOrder.lift (fun (f : NonarchAddGroupNorm E) => ⇑f) ⋯

source
theorem NonarchAddGroupNorm.le_def {E : Type u_3} [AddGroup E] {p q : NonarchAddGroupNorm E} :
p ≤ q ↔ ⇑p ≤ ⇑q
source
theorem NonarchAddGroupNorm.lt_def {E : Type u_3} [AddGroup E] {p q : NonarchAddGroupNorm E} :
p < q ↔ ⇑p < ⇑q
source
@[simp]
theorem NonarchAddGroupNorm.coe_le_coe {E : Type u_3} [AddGroup E] {p q : NonarchAddGroupNorm E} :
⇑p ≤ ⇑q ↔ p ≤ q
source
@[simp]
theorem NonarchAddGroupNorm.coe_lt_coe {E : Type u_3} [AddGroup E] {p q : NonarchAddGroupNorm E} :
⇑p < ⇑q ↔ p < q
source
instance NonarchAddGroupNorm.instMax {E : Type u_3} [AddGroup E] :
Max (NonarchAddGroupNorm E)
Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem NonarchAddGroupNorm.coe_sup {E : Type u_3} [AddGroup E] (p q : NonarchAddGroupNorm E) :
⇑(p ⊔ q) = ⇑p ⊔ ⇑q
source
@[simp]
theorem NonarchAddGroupNorm.sup_apply {E : Type u_3} [AddGroup E] (p q : NonarchAddGroupNorm E) (x : E) :
(p ⊔ q) x = max (p x) (q x)
source
noncomputable instance NonarchAddGroupNorm.instSemilatticeSup {E : Type u_3} [AddGroup E] :
SemilatticeSup (NonarchAddGroupNorm E)
Equations

- NonarchAddGroupNorm.instSemilatticeSup = Function.Injective.semilatticeSup (fun (f : NonarchAddGroupNorm E) => ⇑f) ⋯ ⋯

source
instance NonarchAddGroupNorm.instOneOfDecidableEq {E : Type u_3} [AddGroup E] [DecidableEq E] :
One (NonarchAddGroupNorm E)
Equations

- NonarchAddGroupNorm.instOneOfDecidableEq = { one := let __src := 1; { toNonarchAddGroupSeminorm := __src, eq_zero_of_map_eq_zero' := ⋯ } }

source
@[simp]
theorem NonarchAddGroupNorm.apply_one {E : Type u_3} [AddGroup E] [DecidableEq E] (x : E) :
1 x = if x = 0 then 0 else 1
source
instance NonarchAddGroupNorm.instInhabitedOfDecidableEq {E : Type u_3} [AddGroup E] [DecidableEq E] :
Inhabited (NonarchAddGroupNorm E)
Equations

- NonarchAddGroupNorm.instInhabitedOfDecidableEq = { default := 1 }