Hamming

📁 Source: Mathlib/InformationTheory/Hamming.lean

Statistics

Metric	Count
Definitions `Hamming`, `instAdd`, `instAddCommGroup`, `instAddCommMonoid`, `instAddGroup`, `instAddMonoid`, `instDecidableEqOfFintype`, `instDist`, `instFintypeOfDecidableEq`, `instInhabited`, `instMetricSpace`, `instModule`, `instNeg`, `instNormOfZero`, `instNormedAddCommGroupOfAddCommGroup`, `instNormedAddGroupOfAddGroup`, `instPseudoMetricSpace`, `instSMul`, `instSMulWithZero`, `instSub`, `instZero`, `ofHamming`, `toHamming`, `hammingDist`, `hammingNorm`	25
Theorems `dist_eq_hammingDist`, `instDiscreteTopology`, `instNontrivialOfNonemptyOfDefault`, `nndist_eq_hammingDist`, `nnnorm_eq_hammingNorm`, `norm_eq_hammingNorm`, `ofHamming_add`, `ofHamming_inj`, `ofHamming_neg`, `ofHamming_smul`, `ofHamming_sub`, `ofHamming_symm_eq`, `ofHamming_toHamming`, `ofHamming_zero`, `toHamming_add`, `toHamming_inj`, `toHamming_neg`, `toHamming_ofHamming`, `toHamming_smul`, `toHamming_sub`, `toHamming_symm_eq`, `toHamming_zero`, `eq_of_hammingDist_eq_zero`, `hammingDist_comm`, `hammingDist_comp`, `hammingDist_comp_le_hammingDist`, `hammingDist_eq_hammingNorm`, `hammingDist_eq_zero`, `hammingDist_le_card_fintype`, `hammingDist_lt_one`, `hammingDist_ne_zero`, `hammingDist_nonneg`, `hammingDist_pos`, `hammingDist_self`, `hammingDist_smul`, `hammingDist_smul_le_hammingDist`, `hammingDist_triangle`, `hammingDist_triangle_left`, `hammingDist_triangle_right`, `hammingDist_zero_left`, `hammingDist_zero_right`, `hammingNorm_comp`, `hammingNorm_comp_le_hammingNorm`, `hammingNorm_eq_zero`, `hammingNorm_le_card_fintype`, `hammingNorm_lt_one`, `hammingNorm_ne_zero_iff`, `hammingNorm_nonneg`, `hammingNorm_pos_iff`, `hammingNorm_smul`, `hammingNorm_smul_le_hammingNorm`, `hammingNorm_zero`, `hamming_zero_eq_dist`, `swap_hammingDist`	54
Total	79

Hamming

Definitions

Name	Category	Theorems
`instAdd` 📖	CompOp	2 math math: `toHamming_add`, `ofHamming_add`
`instAddCommGroup` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	—
`instAddGroup` 📖	CompOp	—
`instAddMonoid` 📖	CompOp	—
`instDecidableEqOfFintype` 📖	CompOp	—
`instDist` 📖	CompOp	1 math math: `dist_eq_hammingDist`
`instFintypeOfDecidableEq` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instMetricSpace` 📖	CompOp	—
`instModule` 📖	CompOp	—
`instNeg` 📖	CompOp	2 math math: `ofHamming_neg`, `toHamming_neg`
`instNormOfZero` 📖	CompOp	1 math math: `norm_eq_hammingNorm`
`instNormedAddCommGroupOfAddCommGroup` 📖	CompOp	—
`instNormedAddGroupOfAddGroup` 📖	CompOp	1 math math: `nnnorm_eq_hammingNorm`
`instPseudoMetricSpace` 📖	CompOp	2 math math: `nndist_eq_hammingDist`, `instDiscreteTopology`
`instSMul` 📖	CompOp	2 math math: `ofHamming_smul`, `toHamming_smul`
`instSMulWithZero` 📖	CompOp	—
`instSub` 📖	CompOp	2 math math: `toHamming_sub`, `ofHamming_sub`
`instZero` 📖	CompOp	2 math math: `ofHamming_zero`, `toHamming_zero`
`ofHamming` 📖	CompOp	14 math math: `ofHamming_zero`, `nndist_eq_hammingDist`, `ofHamming_smul`, `nnnorm_eq_hammingNorm`, `ofHamming_sub`, `ofHamming_add`, `toHamming_symm_eq`, `norm_eq_hammingNorm`, `ofHamming_inj`, `ofHamming_toHamming`, `ofHamming_symm_eq`, `dist_eq_hammingDist`, `ofHamming_neg`, `toHamming_ofHamming`
`toHamming` 📖	CompOp	10 math math: `toHamming_sub`, `toHamming_smul`, `toHamming_add`, `toHamming_symm_eq`, `ofHamming_toHamming`, `ofHamming_symm_eq`, `toHamming_zero`, `toHamming_inj`, `toHamming_neg`, `toHamming_ofHamming`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_eq_hammingDist` 📖	mathematical	—	`Dist.dist` `Hamming` `instDist` `Real` `Real.instNatCast` `hammingDist` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofHamming`	—	—
`instDiscreteTopology` 📖	mathematical	—	`DiscreteTopology` `Hamming` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpace`	—	—
`instNontrivialOfNonemptyOfDefault` 📖	mathematical	—	`Nontrivial` `Hamming`	—	`Pi.nontrivial`
`nndist_eq_hammingDist` 📖	mathematical	—	`NNDist.nndist` `Hamming` `PseudoMetricSpace.toNNDist` `instPseudoMetricSpace` `NNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `hammingDist` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofHamming`	—	—
`nnnorm_eq_hammingNorm` 📖	mathematical	—	`NNNorm.nnnorm` `Hamming` `SeminormedAddGroup.toNNNorm` `NormedAddGroup.toSeminormedAddGroup` `instNormedAddGroupOfAddGroup` `NNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `hammingNorm` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofHamming`	—	—
`norm_eq_hammingNorm` 📖	mathematical	—	`Norm.norm` `Hamming` `instNormOfZero` `Real` `Real.instNatCast` `hammingNorm` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofHamming`	—	—
`ofHamming_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Hamming` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofHamming` `instAdd` `Pi.instAdd`	—	—
`ofHamming_inj` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Hamming` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofHamming`	—	—
`ofHamming_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Hamming` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofHamming` `instNeg` `Pi.instNeg`	—	—
`ofHamming_smul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Hamming` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofHamming` `instSMul` `Pi.instSMul`	—	—
`ofHamming_sub` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Hamming` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofHamming` `instSub` `Pi.instSub`	—	—
`ofHamming_symm_eq` 📖	mathematical	—	`Equiv.symm` `Hamming` `ofHamming` `toHamming`	—	—
`ofHamming_toHamming` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Hamming` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofHamming` `toHamming`	—	—
`ofHamming_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Hamming` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofHamming` `instZero` `Pi.instZero`	—	—
`toHamming_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Hamming` `EquivLike.toFunLike` `Equiv.instEquivLike` `toHamming` `Pi.instAdd` `instAdd`	—	—
`toHamming_inj` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Hamming` `EquivLike.toFunLike` `Equiv.instEquivLike` `toHamming`	—	—
`toHamming_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Hamming` `EquivLike.toFunLike` `Equiv.instEquivLike` `toHamming` `Pi.instNeg` `instNeg`	—	—
`toHamming_ofHamming` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Hamming` `EquivLike.toFunLike` `Equiv.instEquivLike` `toHamming` `ofHamming`	—	—
`toHamming_smul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Hamming` `EquivLike.toFunLike` `Equiv.instEquivLike` `toHamming` `Pi.instSMul` `instSMul`	—	—
`toHamming_sub` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Hamming` `EquivLike.toFunLike` `Equiv.instEquivLike` `toHamming` `Pi.instSub` `instSub`	—	—
`toHamming_symm_eq` 📖	mathematical	—	`Equiv.symm` `Hamming` `toHamming` `ofHamming`	—	—
`toHamming_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Hamming` `EquivLike.toFunLike` `Equiv.instEquivLike` `toHamming` `Pi.instZero` `instZero`	—	—

(root)

Definitions

Name	Category	Theorems
`Hamming` 📖	CompOp	22 math math: `Hamming.toHamming_sub`, `Hamming.ofHamming_zero`, `Hamming.instNontrivialOfNonemptyOfDefault`, `Hamming.nndist_eq_hammingDist`, `Hamming.ofHamming_smul`, `Hamming.nnnorm_eq_hammingNorm`, `Hamming.ofHamming_sub`, `Hamming.toHamming_smul`, `Hamming.toHamming_add`, `Hamming.ofHamming_add`, `Hamming.toHamming_symm_eq`, `Hamming.norm_eq_hammingNorm`, `Hamming.ofHamming_inj`, `Hamming.ofHamming_toHamming`, `Hamming.ofHamming_symm_eq`, `Hamming.toHamming_zero`, `Hamming.dist_eq_hammingDist`, `Hamming.toHamming_inj`, `Hamming.ofHamming_neg`, `Hamming.toHamming_neg`, `Hamming.instDiscreteTopology`, `Hamming.toHamming_ofHamming`
`hammingDist` 📖	CompOp	21 math math: `hammingDist_self`, `hammingDist_comp`, `hammingDist_smul`, `hammingDist_triangle_right`, `hammingDist_triangle`, `hammingDist_eq_zero`, `Hamming.nndist_eq_hammingDist`, `hammingDist_smul_le_hammingDist`, `hammingDist_zero_right`, `hammingDist_pos`, `hammingDist_comp_le_hammingDist`, `hammingDist_lt_one`, `swap_hammingDist`, `hammingDist_nonneg`, `hammingDist_comm`, `Hamming.dist_eq_hammingDist`, `hammingDist_zero_left`, `hammingDist_eq_hammingNorm`, `hammingDist_triangle_left`, `hammingDist_le_card_fintype`, `hamming_zero_eq_dist`
`hammingNorm` 📖	CompOp	15 math math: `hammingNorm_pos_iff`, `Hamming.nnnorm_eq_hammingNorm`, `hammingNorm_comp`, `hammingNorm_le_card_fintype`, `hammingDist_zero_right`, `hammingNorm_eq_zero`, `hammingNorm_smul_le_hammingNorm`, `Hamming.norm_eq_hammingNorm`, `hammingNorm_zero`, `hammingNorm_smul`, `hammingNorm_nonneg`, `hammingNorm_lt_one`, `hammingDist_zero_left`, `hammingDist_eq_hammingNorm`, `hammingNorm_comp_le_hammingNorm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_hammingDist_eq_zero` 📖	—	`hammingDist`	—	—	—
`hammingDist_comm` 📖	mathematical	—	`hammingDist`	—	`Finset.filter.congr_simp`
`hammingDist_comp` 📖	mathematical	—	`hammingDist`	—	`le_antisymm` `hammingDist_comp_le_hammingDist` `Finset.card_le_card` `Finset.monotone_filter_right`
`hammingDist_comp_le_hammingDist` 📖	mathematical	—	`hammingDist`	—	`Finset.card_le_card` `Finset.monotone_filter_right`
`hammingDist_eq_hammingNorm` 📖	mathematical	—	`hammingDist` `hammingNorm` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`Finset.filter.congr_simp`
`hammingDist_eq_zero` 📖	mathematical	—	`hammingDist`	—	`eq_of_hammingDist_eq_zero` `hammingDist_self`
`hammingDist_le_card_fintype` 📖	mathematical	—	`hammingDist` `Fintype.card`	—	`Finset.card_le_univ`
`hammingDist_lt_one` 📖	mathematical	—	`hammingDist`	—	`hammingDist_eq_zero`
`hammingDist_ne_zero` 📖	—	—	—	—	`Iff.not` `hammingDist_eq_zero`
`hammingDist_nonneg` 📖	mathematical	—	`hammingDist`	—	`zero_le` `Nat.instCanonicallyOrderedAdd`
`hammingDist_pos` 📖	mathematical	—	`hammingDist`	—	`hammingDist_ne_zero` `iff_not_comm` `not_lt`
`hammingDist_self` 📖	mathematical	—	`hammingDist`	—	`hammingDist.eq_1` `Finset.card_eq_zero` `Finset.filter_eq_empty_iff`
`hammingDist_smul` 📖	mathematical	`IsSMulRegular`	`hammingDist` `Pi.instSMul`	—	`hammingDist_comp`
`hammingDist_smul_le_hammingDist` 📖	mathematical	—	`hammingDist` `Pi.instSMul`	—	`hammingDist_comp_le_hammingDist`
`hammingDist_triangle` 📖	mathematical	—	`hammingDist`	—	`le_trans` `Finset.card_mono` `Finset.filter_or` `Finset.monotone_filter_right` `Ne.ne_or_ne` `Finset.card_union_le`
`hammingDist_triangle_left` 📖	mathematical	—	`hammingDist`	—	`hammingDist_comm` `hammingDist_triangle`
`hammingDist_triangle_right` 📖	mathematical	—	`hammingDist`	—	`hammingDist_comm` `hammingDist_triangle`
`hammingDist_zero_left` 📖	mathematical	—	`hammingDist` `Pi.instZero` `hammingNorm`	—	`hammingDist_comm` `hammingDist_zero_right`
`hammingDist_zero_right` 📖	mathematical	—	`hammingDist` `Pi.instZero` `hammingNorm`	—	—
`hammingNorm_comp` 📖	mathematical	—	`hammingNorm`	—	`hammingDist.congr_simp` `hammingDist_comp`
`hammingNorm_comp_le_hammingNorm` 📖	mathematical	—	`hammingNorm`	—	`hammingDist.congr_simp` `hammingDist_comp_le_hammingDist`
`hammingNorm_eq_zero` 📖	mathematical	—	`hammingNorm` `Pi.instZero`	—	`hammingDist_eq_zero`
`hammingNorm_le_card_fintype` 📖	mathematical	—	`hammingNorm` `Fintype.card`	—	`hammingDist_le_card_fintype`
`hammingNorm_lt_one` 📖	mathematical	—	`hammingNorm` `Pi.instZero`	—	`hammingDist_lt_one`
`hammingNorm_ne_zero_iff` 📖	—	—	—	—	`Iff.not` `hammingNorm_eq_zero`
`hammingNorm_nonneg` 📖	mathematical	—	`hammingNorm`	—	`zero_le` `Nat.instCanonicallyOrderedAdd`
`hammingNorm_pos_iff` 📖	mathematical	—	`hammingNorm`	—	`hammingDist_pos`
`hammingNorm_smul` 📖	mathematical	`IsSMulRegular` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	`hammingNorm` `Pi.instSMul`	—	`hammingNorm_comp` `smul_zero`
`hammingNorm_smul_le_hammingNorm` 📖	mathematical	—	`hammingNorm` `Pi.instSMul` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	—	`hammingNorm_comp_le_hammingNorm` `smul_zero`
`hammingNorm_zero` 📖	mathematical	—	`hammingNorm` `Pi.instZero`	—	`hammingDist_self`
`hamming_zero_eq_dist` 📖	mathematical	—	`hammingDist`	—	`hammingDist_eq_zero`
`swap_hammingDist` 📖	mathematical	—	`Function.swap` `hammingDist`	—	`hammingDist_comm`

---

← Back to Index