Theorems · Theorem · functional analysis

AddChar.norm_apply

∀ {α : Type u_1} [inst : NormedRing α] [NormMulClass α] [NormOneClass α] {G : Type u_3} [inst_3 : AddLeftCancelMonoid G]
  [Finite G] (ψ : AddChar G α) (x : G), ‖ψ x‖ = 1

Defined in

Mathlib.Analysis.Normed.Ring.Finite

Cited by

2 results in Mathlib

Foundations

Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedRingNormMulClassNormOneClassAddLeftCancelMonoidFinite