Documentation Verification Report

Normalize

📁 Source: Mathlib/Analysis/Normed/Module/Normalize.lean

Statistics

Metric	Count
Definitions `normalize`	1
Theorems `norm_normalize`, `norm_normalize_eq_one_iff`, `norm_smul_normalize`, `normalize_eq_self_of_norm_eq_one`, `normalize_eq_zero_iff`, `normalize_neg`, `normalize_normalize`, `normalize_smul`, `normalize_smul_of_neg`, `normalize_smul_of_pos`, `normalize_zero_eq_zero`	11
Total	12

NormedSpace

Definitions

Name	Category	Theorems
`normalize` 📖	CompOp	21 math math: `InnerProductGeometry.angle_normalize_left`, `InnerProductGeometry.angle_normalize_right`, `signedDist_linear_apply_apply`, `signedDist_apply_apply`, `normalize_smul`, `normalize_eq_self_of_norm_eq_one`, `normalize_smul_of_pos`, `signedDist_vadd_right`, `normalize_smul_of_neg`, `normalize_eq_zero_iff`, `normalize_normalize`, `signedDist_linear_apply`, `signedDist_vadd_left`, `signedDist_apply_linear_apply`, `normalize_zero_eq_zero`, `signedDist_apply`, `norm_smul_normalize`, `norm_normalize`, `signedDist_apply_linear`, `normalize_neg`, `norm_normalize_eq_one_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_normalize` 📖	mathematical	—	`Norm.norm` `NormedAddCommGroup.toNorm` `normalize` `Real` `Real.instOne`	—	`norm_normalize_eq_one_iff`
`norm_normalize_eq_one_iff` 📖	mathematical	—	`Norm.norm` `NormedAddCommGroup.toNorm` `normalize` `Real` `Real.instOne`	—	`norm_zero` `inv_zero` `smul_zero` `NeZero.charZero_one` `RCLike.charZero_rclike` `norm_smul` `toNormSMulClass` `norm_inv` `norm_norm` `inv_mul_cancel₀`
`norm_smul_normalize` 📖	mathematical	—	`Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `toModule` `Real.normedField` `Norm.norm` `NormedAddCommGroup.toNorm` `normalize`	—	`norm_zero` `inv_zero` `smul_zero` `smul_inv_smul₀`
`normalize_eq_self_of_norm_eq_one` 📖	mathematical	`Norm.norm` `NormedAddCommGroup.toNorm` `Real` `Real.instOne`	`normalize`	—	`inv_one` `one_smul`
`normalize_eq_zero_iff` 📖	mathematical	—	`normalize` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`norm_zero` `inv_zero` `smul_zero`
`normalize_neg` 📖	mathematical	—	`normalize` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`norm_neg` `smul_neg`
`normalize_normalize` 📖	mathematical	—	`normalize`	—	`normalize_zero_eq_zero` `normalize_eq_self_of_norm_eq_one`
`normalize_smul` 📖	mathematical	—	`normalize` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `toModule` `Real.normedField` `SignType.cast` `Real.instZero` `Real.instOne` `Real.instNeg` `DFunLike.coe` `OrderHom` `SignType` `Real.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `Real.decidableLT`	—	`lt_trichotomy` `normalize_smul_of_pos` `sign_pos` `one_smul` `zero_smul` `normalize_zero_eq_zero` `sign_zero` `normalize_smul_of_neg` `sign_neg` `SignType.coe_neg` `neg_smul`
`normalize_smul_of_neg` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`normalize` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `toModule` `Real.normedField` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`smul_neg` `neg_smul` `neg_neg` `normalize_neg` `normalize_smul_of_pos` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le`
`normalize_smul_of_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`normalize` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `toModule` `Real.normedField`	—	`norm_smul` `toNormSMulClass` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_inv_rev` `smul_smul` `inv_mul_cancel_right₀` `LT.lt.ne'`
`normalize_zero_eq_zero` 📖	mathematical	—	`normalize` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`norm_zero` `inv_zero` `smul_zero`

---

← Back to Index