mathlib3 documentation

information_theory.hamming

Hamming spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The Hamming metric counts the number of places two members of a (finite) Pi type differ. The Hamming norm is the same as the Hamming metric over additive groups, and counts the number of places a member of a (finite) Pi type differs from zero.

This is a useful notion in various applications, but in particular it is relevant in coding theory, in which it is fundamental for defining the minimum distance of a code.

Main definitions #

hamming_dist x y: the Hamming distance between x and y, the number of entries which differ.
hamming_norm x: the Hamming norm of x, the number of non-zero entries.
hamming β: a type synonym for Π i, β i with dist and norm provided by the above.
hamming.to_hamming, hamming.of_hamming: functions for casting between hamming β and Π i, β i.
hamming.normed_add_comm_group: the Hamming norm forms a normed group on hamming β.

def hamming_dist {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] (x y : Π (i : ι), β i) :

The Hamming distance function to the naturals.

Equations

hamming_dist x y = (finset.filter (λ (i : ι), x i ≠ y i) finset.univ).card

@[simp]

theorem hamming_dist_self {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] (x : Π (i : ι), β i) :

hamming_dist x x = 0

Corresponds to dist_self.

theorem hamming_dist_nonneg {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {x y : Π (i : ι), β i} :

0 ≤ hamming_dist x y

Corresponds to dist_nonneg.

theorem hamming_dist_comm {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] (x y : Π (i : ι), β i) :

hamming_dist x y = hamming_dist y x

Corresponds to dist_comm.

theorem hamming_dist_triangle {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] (x y z : Π (i : ι), β i) :

hamming_dist x z ≤ hamming_dist x y + hamming_dist y z

Corresponds to dist_triangle.

theorem hamming_dist_triangle_left {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] (x y z : Π (i : ι), β i) :

hamming_dist x y ≤ hamming_dist z x + hamming_dist z y

Corresponds to dist_triangle_left.

theorem hamming_dist_triangle_right {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] (x y z : Π (i : ι), β i) :

hamming_dist x y ≤ hamming_dist x z + hamming_dist y z

Corresponds to dist_triangle_right.

theorem swap_hamming_dist {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] :

function.swap hamming_dist = hamming_dist

Corresponds to swap_dist.

theorem eq_of_hamming_dist_eq_zero {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {x y : Π (i : ι), β i} :

hamming_dist x y = 0 → x = y

Corresponds to eq_of_dist_eq_zero.

@[simp]

theorem hamming_dist_eq_zero {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {x y : Π (i : ι), β i} :

hamming_dist x y = 0 ↔ x = y

Corresponds to dist_eq_zero.

@[simp]

theorem hamming_zero_eq_dist {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {x y : Π (i : ι), β i} :

0 = hamming_dist x y ↔ x = y

Corresponds to zero_eq_dist.

theorem hamming_dist_ne_zero {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {x y : Π (i : ι), β i} :

hamming_dist x y ≠ 0 ↔ x ≠ y

Corresponds to dist_ne_zero.

@[simp]

theorem hamming_dist_pos {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {x y : Π (i : ι), β i} :

0 < hamming_dist x y ↔ x ≠ y

Corresponds to dist_pos.

@[simp]

theorem hamming_dist_lt_one {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {x y : Π (i : ι), β i} :

hamming_dist x y < 1 ↔ x = y

theorem hamming_dist_le_card_fintype {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {x y : Π (i : ι), β i} :

hamming_dist x y ≤ fintype.card ι

theorem hamming_dist_comp_le_hamming_dist {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {γ : ι → Type u_4} [Π (i : ι), decidable_eq (γ i)] (f : Π (i : ι), γ i → β i) {x y : Π (i : ι), γ i} :

hamming_dist (λ (i : ι), f i (x i)) (λ (i : ι), f i (y i)) ≤ hamming_dist x y

theorem hamming_dist_comp {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {γ : ι → Type u_4} [Π (i : ι), decidable_eq (γ i)] (f : Π (i : ι), γ i → β i) {x y : Π (i : ι), γ i} (hf : ∀ (i : ι), function.injective (f i)) :

hamming_dist (λ (i : ι), f i (x i)) (λ (i : ι), f i (y i)) = hamming_dist x y

theorem hamming_dist_smul_le_hamming_dist {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_smul α (β i)] {k : α} {x y : Π (i : ι), β i} :

hamming_dist (k • x) (k • y) ≤ hamming_dist x y

theorem hamming_dist_smul {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_smul α (β i)] {k : α} {x y : Π (i : ι), β i} (hk : ∀ (i : ι), is_smul_regular (β i) k) :

hamming_dist (k • x) (k • y) = hamming_dist x y

Corresponds to dist_smul with the discrete norm on α.

def hamming_norm {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] (x : Π (i : ι), β i) :

The Hamming weight function to the naturals.

Equations

hamming_norm x = (finset.filter (λ (i : ι), x i ≠ 0) finset.univ).card

@[simp]

theorem hamming_dist_zero_right {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] (x : Π (i : ι), β i) :

hamming_dist x 0 = hamming_norm x

Corresponds to dist_zero_right.

@[simp]

theorem hamming_dist_zero_left {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] :

hamming_dist 0 = hamming_norm

Corresponds to dist_zero_left.

@[simp]

theorem hamming_norm_nonneg {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] {x : Π (i : ι), β i} :

0 ≤ hamming_norm x

Corresponds to norm_nonneg.

@[simp]

theorem hamming_norm_zero {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] :

hamming_norm 0 = 0

Corresponds to norm_zero.

@[simp]

theorem hamming_norm_eq_zero {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] {x : Π (i : ι), β i} :

hamming_norm x = 0 ↔ x = 0

Corresponds to norm_eq_zero.

theorem hamming_norm_ne_zero_iff {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] {x : Π (i : ι), β i} :

hamming_norm x ≠ 0 ↔ x ≠ 0

Corresponds to norm_ne_zero_iff.

@[simp]

theorem hamming_norm_pos_iff {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] {x : Π (i : ι), β i} :

0 < hamming_norm x ↔ x ≠ 0

Corresponds to norm_pos_iff.

@[simp]

theorem hamming_norm_lt_one {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] {x : Π (i : ι), β i} :

hamming_norm x < 1 ↔ x = 0

theorem hamming_norm_le_card_fintype {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] {x : Π (i : ι), β i} :

hamming_norm x ≤ fintype.card ι

theorem hamming_norm_comp_le_hamming_norm {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {γ : ι → Type u_4} [Π (i : ι), decidable_eq (γ i)] [Π (i : ι), has_zero (β i)] [Π (i : ι), has_zero (γ i)] (f : Π (i : ι), γ i → β i) {x : Π (i : ι), γ i} (hf : ∀ (i : ι), f i 0 = 0) :

hamming_norm (λ (i : ι), f i (x i)) ≤ hamming_norm x

theorem hamming_norm_comp {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {γ : ι → Type u_4} [Π (i : ι), decidable_eq (γ i)] [Π (i : ι), has_zero (β i)] [Π (i : ι), has_zero (γ i)] (f : Π (i : ι), γ i → β i) {x : Π (i : ι), γ i} (hf₁ : ∀ (i : ι), function.injective (f i)) (hf₂ : ∀ (i : ι), f i 0 = 0) :

hamming_norm (λ (i : ι), f i (x i)) = hamming_norm x

theorem hamming_norm_smul_le_hamming_norm {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] [has_zero α] [Π (i : ι), smul_with_zero α (β i)] {k : α} {x : Π (i : ι), β i} :

hamming_norm (k • x) ≤ hamming_norm x

theorem hamming_norm_smul {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] [has_zero α] [Π (i : ι), smul_with_zero α (β i)] {k : α} (hk : ∀ (i : ι), is_smul_regular (β i) k) (x : Π (i : ι), β i) :

hamming_norm (k • x) = hamming_norm x

theorem hamming_dist_eq_hamming_norm {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), add_group (β i)] (x y : Π (i : ι), β i) :

hamming_dist x y = hamming_norm (x - y)

Corresponds to dist_eq_norm.

The `hamming` type synonym #

def hamming {ι : Type u_1} (β : ι → Type u_2) :

Type (max u_1 u_2)

Type synonym for a Pi type which inherits the usual algebraic instances, but is equipped with the Hamming metric and norm, instead of pi.normed_add_comm_group which uses the sup norm.

Equations

hamming β = Π (i : ι), β i

Instances for hamming

Instances inherited from normal Pi types.

@[protected, instance]

def hamming.inhabited {ι : Type u_2} {β : ι → Type u_3} [Π (i : ι), inhabited (β i)] :

inhabited (hamming β)

Equations

hamming.inhabited = {default := λ (i : ι), inhabited.default}

@[protected, instance]

def hamming.fintype {ι : Type u_2} {β : ι → Type u_3} [decidable_eq ι] [fintype ι] [Π (i : ι), fintype (β i)] :

fintype (hamming β)

Equations

hamming.fintype = pi.fintype

@[protected, instance]

def hamming.nontrivial {ι : Type u_2} {β : ι → Type u_3} [inhabited ι] [∀ (i : ι), nonempty (β i)] [nontrivial (β inhabited.default)] :

nontrivial (hamming β)

@[protected, instance]

def hamming.decidable_eq {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] :

decidable_eq (hamming β)

Equations

hamming.decidable_eq = fintype.decidable_pi_fintype

@[protected, instance]

def hamming.has_zero {ι : Type u_2} {β : ι → Type u_3} [Π (i : ι), has_zero (β i)] :

has_zero (hamming β)

Equations

hamming.has_zero = pi.has_zero

@[protected, instance]

def hamming.has_neg {ι : Type u_2} {β : ι → Type u_3} [Π (i : ι), has_neg (β i)] :

has_neg (hamming β)

Equations

hamming.has_neg = pi.has_neg

@[protected, instance]

def hamming.has_add {ι : Type u_2} {β : ι → Type u_3} [Π (i : ι), has_add (β i)] :

has_add (hamming β)

Equations

hamming.has_add = pi.has_add

@[protected, instance]

def hamming.has_sub {ι : Type u_2} {β : ι → Type u_3} [Π (i : ι), has_sub (β i)] :

has_sub (hamming β)

Equations

hamming.has_sub = pi.has_sub

@[protected, instance]

def hamming.has_smul {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [Π (i : ι), has_smul α (β i)] :

has_smul α (hamming β)

Equations

hamming.has_smul = pi.has_smul

@[protected, instance]

def hamming.smul_with_zero {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [has_zero α] [Π (i : ι), has_zero (β i)] [Π (i : ι), smul_with_zero α (β i)] :

smul_with_zero α (hamming β)

Equations

hamming.smul_with_zero = pi.smul_with_zero α

@[protected, instance]

def hamming.add_monoid {ι : Type u_2} {β : ι → Type u_3} [Π (i : ι), add_monoid (β i)] :

add_monoid (hamming β)

Equations

hamming.add_monoid = pi.add_monoid

@[protected, instance]

def hamming.add_comm_monoid {ι : Type u_2} {β : ι → Type u_3} [Π (i : ι), add_comm_monoid (β i)] :

add_comm_monoid (hamming β)

Equations

hamming.add_comm_monoid = pi.add_comm_monoid

@[protected, instance]

def hamming.add_comm_group {ι : Type u_2} {β : ι → Type u_3} [Π (i : ι), add_comm_group (β i)] :

add_comm_group (hamming β)

Equations

hamming.add_comm_group = pi.add_comm_group

@[protected, instance]

def hamming.module {ι : Type u_2} (α : Type u_1) [semiring α] (β : ι → Type u_3) [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), module α (β i)] :

module α (hamming β)

Equations

hamming.module α β = pi.module ι (λ (i : ι), β i) α

API to/from the type synonym.

def hamming.to_hamming {ι : Type u_2} {β : ι → Type u_3} :

(Π (i : ι), β i) ≃ hamming β

to_hamming is the identity function to the hamming of a type.

Equations

hamming.to_hamming = equiv.refl (Π (i : ι), β i)

def hamming.of_hamming {ι : Type u_2} {β : ι → Type u_3} :

hamming β ≃ Π (i : ι), β i

of_hamming is the identity function from the hamming of a type.

Equations

hamming.of_hamming = equiv.refl (hamming β)

@[simp]

theorem hamming.to_hamming_symm_eq {ι : Type u_2} {β : ι → Type u_3} :

hamming.to_hamming.symm = hamming.of_hamming

@[simp]

theorem hamming.of_hamming_symm_eq {ι : Type u_2} {β : ι → Type u_3} :

hamming.of_hamming.symm = hamming.to_hamming

@[simp]

theorem hamming.to_hamming_of_hamming {ι : Type u_2} {β : ι → Type u_3} (x : hamming β) :

⇑hamming.to_hamming (⇑hamming.of_hamming x) = x

@[simp]

theorem hamming.of_hamming_to_hamming {ι : Type u_2} {β : ι → Type u_3} (x : Π (i : ι), β i) :

⇑hamming.of_hamming (⇑hamming.to_hamming x) = x

@[simp]

theorem hamming.to_hamming_inj {ι : Type u_2} {β : ι → Type u_3} {x y : Π (i : ι), β i} :

⇑hamming.to_hamming x = ⇑hamming.to_hamming y ↔ x = y

@[simp]

theorem hamming.of_hamming_inj {ι : Type u_2} {β : ι → Type u_3} {x y : hamming β} :

⇑hamming.of_hamming x = ⇑hamming.of_hamming y ↔ x = y

@[simp]

theorem hamming.to_hamming_zero {ι : Type u_2} {β : ι → Type u_3} [Π (i : ι), has_zero (β i)] :

⇑hamming.to_hamming 0 = 0

@[simp]

theorem hamming.of_hamming_zero {ι : Type u_2} {β : ι → Type u_3} [Π (i : ι), has_zero (β i)] :

⇑hamming.of_hamming 0 = 0

@[simp]

theorem hamming.to_hamming_neg {ι : Type u_2} {β : ι → Type u_3} [Π (i : ι), has_neg (β i)] {x : Π (i : ι), β i} :

⇑hamming.to_hamming (-x) = -⇑hamming.to_hamming x

@[simp]

theorem hamming.of_hamming_neg {ι : Type u_2} {β : ι → Type u_3} [Π (i : ι), has_neg (β i)] {x : hamming β} :

⇑hamming.of_hamming (-x) = -⇑hamming.of_hamming x

@[simp]

theorem hamming.to_hamming_add {ι : Type u_2} {β : ι → Type u_3} [Π (i : ι), has_add (β i)] {x y : Π (i : ι), β i} :

⇑hamming.to_hamming (x + y) = ⇑hamming.to_hamming x + ⇑hamming.to_hamming y

@[simp]

theorem hamming.of_hamming_add {ι : Type u_2} {β : ι → Type u_3} [Π (i : ι), has_add (β i)] {x y : hamming β} :

⇑hamming.of_hamming (x + y) = ⇑hamming.of_hamming x + ⇑hamming.of_hamming y

@[simp]

theorem hamming.to_hamming_sub {ι : Type u_2} {β : ι → Type u_3} [Π (i : ι), has_sub (β i)] {x y : Π (i : ι), β i} :

⇑hamming.to_hamming (x - y) = ⇑hamming.to_hamming x - ⇑hamming.to_hamming y

@[simp]

theorem hamming.of_hamming_sub {ι : Type u_2} {β : ι → Type u_3} [Π (i : ι), has_sub (β i)] {x y : hamming β} :

⇑hamming.of_hamming (x - y) = ⇑hamming.of_hamming x - ⇑hamming.of_hamming y

@[simp]

theorem hamming.to_hamming_smul {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [Π (i : ι), has_smul α (β i)] {r : α} {x : Π (i : ι), β i} :

⇑hamming.to_hamming (r • x) = r • ⇑hamming.to_hamming x

@[simp]

theorem hamming.of_hamming_smul {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [Π (i : ι), has_smul α (β i)] {r : α} {x : hamming β} :

⇑hamming.of_hamming (r • x) = r • ⇑hamming.of_hamming x

Instances equipping hamming with hamming_norm and hamming_dist.

@[protected, instance]

def hamming.has_dist {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] :

has_dist (hamming β)

Equations

hamming.has_dist = {dist := λ (x y : hamming β), ↑(hamming_dist (⇑hamming.of_hamming x) (⇑hamming.of_hamming y))}

@[simp]

theorem hamming.dist_eq_hamming_dist {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] (x y : hamming β) :

has_dist.dist x y = ↑(hamming_dist (⇑hamming.of_hamming x) (⇑hamming.of_hamming y))

@[protected, instance]

def hamming.pseudo_metric_space {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] :

pseudo_metric_space (hamming β)

Equations

hamming.pseudo_metric_space = {to_has_dist := {dist := has_dist.dist hamming.has_dist}, dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : hamming β), ↑⟨has_dist.dist x y, _⟩, edist_dist := _, to_uniform_space := ⊥, uniformity_dist := _, to_bornology := {cobounded := ⊥, le_cofinite := _}, cobounded_sets := _}

@[simp]

theorem hamming.nndist_eq_hamming_dist {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] (x y : hamming β) :

has_nndist.nndist x y = ↑(hamming_dist (⇑hamming.of_hamming x) (⇑hamming.of_hamming y))

@[protected, instance]

def hamming.metric_space {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] :

metric_space (hamming β)

Equations

@[protected, instance]

def hamming.has_norm {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] :

has_norm (hamming β)

Equations

hamming.has_norm = {norm := λ (x : hamming β), ↑(hamming_norm (⇑hamming.of_hamming x))}

@[simp]

theorem hamming.norm_eq_hamming_norm {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] (x : hamming β) :

‖x‖ = ↑(hamming_norm (⇑hamming.of_hamming x))

@[protected, instance]

def hamming.seminormed_add_comm_group {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), add_comm_group (β i)] :

seminormed_add_comm_group (hamming β)

Equations

hamming.seminormed_add_comm_group = {to_has_norm := hamming.has_norm (λ (i : ι), add_zero_class.to_has_zero (β i)), to_add_comm_group := {add := add_comm_group.add pi.add_comm_group, add_assoc := _, zero := add_comm_group.zero pi.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul pi.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg pi.add_comm_group, sub := add_comm_group.sub pi.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul pi.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}, to_pseudo_metric_space := hamming.pseudo_metric_space (λ (i : ι) (a b : β i), _inst_2 i a b), dist_eq := _}

@[simp]

theorem hamming.nnnorm_eq_hamming_norm {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), add_comm_group (β i)] (x : hamming β) :

‖x‖₊ = ↑(hamming_norm (⇑hamming.of_hamming x))

@[protected, instance]

def hamming.normed_add_comm_group {ι : Type u_2} {β : ι → Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), add_comm_group (β i)] :

normed_add_comm_group (hamming β)

Equations

hamming.normed_add_comm_group = {to_has_norm := seminormed_add_comm_group.to_has_norm hamming.seminormed_add_comm_group, to_add_comm_group := seminormed_add_comm_group.to_add_comm_group hamming.seminormed_add_comm_group, to_metric_space := hamming.metric_space (λ (i : ι) (a b : β i), _inst_2 i a b), dist_eq := _}