Documentation Verification Report

AddCircle

📁 Source: Mathlib/Analysis/Normed/Group/AddCircle.lean

Statistics

Metric	Count
Definitions `instNormedAddCommGroupReal`	1
Theorems `closedBall_eq_univ_of_half_period_le`, `coe_real_preimage_closedBall_eq_iUnion`, `coe_real_preimage_closedBall_inter_eq`, `coe_real_preimage_closedBall_period_zero`, `exists_norm_eq_of_isOfFinAddOrder`, `le_add_order_smul_norm_of_isOfFinAddOrder`, `norm_coe_eq_abs_iff`, `norm_coe_mul`, `norm_div_natCast`, `norm_eq`, `norm_eq'`, `norm_eq_of_zero`, `norm_half_period_eq`, `norm_le_half_period`, `norm_neg_period`, `norm_eq`	16
Total	17

AddCircle

Definitions

Name	Category	Theorems
`instNormedAddCommGroupReal` 📖	CompOp	9 math math: `toCircle_add`, `ergodic_nsmul_add`, `exists_norm_nsmul_le`, `ergodic_add_left`, `ergodic_add_right`, `ergodic_nsmul`, `fourier_add_half_inv_index`, `toCircle_nsmul`, `ergodic_zsmul_add`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closedBall_eq_univ_of_half_period_le` 📖	mathematical	`Real` `Real.instLE` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `abs` `Real.lattice` `Real.instAddGroup` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Metric.closedBall` `AddCircle` `Real.instAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `QuotientAddGroup.instSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `AddSubgroup.zmultiples` `AddCommGroup.toAddGroup` `Set.univ`	—	`Nat.instAtLeastTwoHAddOfNat` `Set.eq_univ_iff_forall` `dist_eq_norm` `LE.le.trans` `norm_le_half_period`
`coe_real_preimage_closedBall_eq_iUnion` 📖	mathematical	—	`Set.preimage` `Real` `HasQuotient.Quotient` `AddSubgroup` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `QuotientAddGroup.instSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Set.iUnion` `Real.pseudoMetricSpace` `Real.instAdd` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `Real.instAddGroup`	—	`eq_or_ne` `coe_real_preimage_closedBall_period_zero` `smul_zero` `add_zero` `Set.iUnion_const` `Set.ext` `dist_eq_norm` `norm_eq` `zsmul_eq_mul` `mul_le_mul_iff_right₀` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `abs_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `inv_ne_zero` `abs_mul` `mul_sub` `mul_comm` `inv_mul_cancel_left₀` `LE.le.trans` `round_le`
`coe_real_preimage_closedBall_inter_eq` 📖	mathematical	`Set` `Real` `Set.instHasSubset` `Metric.closedBall` `Real.pseudoMetricSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `abs` `Real.lattice` `Real.instAddGroup` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Set.instInter` `Set.preimage` `HasQuotient.Quotient` `AddSubgroup` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `SeminormedAddCommGroup.toPseudoMetricSpace` `QuotientAddGroup.instSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instLT` `Real.decidableLT`	—	`Nat.instAtLeastTwoHAddOfNat` `le_or_gt` `eq_or_ne` `coe_real_preimage_closedBall_period_zero` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `zero_div` `not_lt` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Metric.closedBall_subset_closedBall` `closedBall_eq_univ_of_half_period_le` `Set.univ_inter` `Real.closedBall_eq_Icc` `zero_smul` `add_zero` `zsmul_eq_mul` `lt_trichotomy` `Int.cast_le_neg_one_or_one_le_cast_of_ne_zero` `Real.instIsStrictOrderedRing` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.atom_pf` `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.neg_zero` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `mul_nonneg_of_nonpos_of_nonpos` `AddGroup.existsAddOfLE` `IsOrderedRing.toMulPosMono` `covariant_swap_add_of_covariant_add` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `le_of_lt` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `CancelDenoms.sub_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Meta.NormNum.isNat_lt_true` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.mul_eq` `sub_eq_zero_of_eq` `abs_eq_self` `LT.lt.le` `CancelDenoms.add_subst` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.add_nonpos` `Mathlib.Tactic.Linarith.without_one_mul` `CancelDenoms.derive_trans` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_abs_nonneg` `MulZeroClass.mul_zero` `abs_eq_neg_self` `coe_real_preimage_closedBall_eq_iUnion` `Set.iUnion_inter` `Set.iUnion_ite` `Set.iUnion_iUnion_eq_left` `Set.iUnion_empty` `Set.union_empty`
`coe_real_preimage_closedBall_period_zero` 📖	mathematical	—	`Set.preimage` `Real` `HasQuotient.Quotient` `AddSubgroup` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `Real.instZero` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `QuotientAddGroup.instSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.pseudoMetricSpace`	—	`Set.ext` `dist_eq_norm` `norm_eq_of_zero`
`exists_norm_eq_of_isOfFinAddOrder` 📖	mathematical	`IsOfFinAddOrder` `AddCircle` `Real` `Real.instAddCommGroup` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instNormedAddCommGroupReal` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	`Norm.norm` `QuotientAddGroup.instNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `AddSubgroup.zmultiples` `AddCommGroup.toAddGroup` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast` `addOrderOf`	—	`AddSubgroup.normal_of_comm` `exists_gcd_eq_one_of_isOfFinAddOrder` `Real.instIsStrictOrderedRing` `norm_div_natCast`
`le_add_order_smul_norm_of_isOfFinAddOrder` 📖	mathematical	`IsOfFinAddOrder` `AddCircle` `Real` `Real.instAddCommGroup` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instNormedAddCommGroupReal` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	`Real.instLE` `AddMonoid.toNatSMul` `Real.instAddMonoid` `addOrderOf` `Norm.norm` `QuotientAddGroup.instNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `AddSubgroup.zmultiples` `AddCommGroup.toAddGroup`	—	`exists_norm_eq_of_isOfFinAddOrder` `Nat.cast_zero` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `LT.lt.ne'` `addOrderOf_pos_iff` `mul_one` `nsmul_eq_mul` `mul_assoc` `mul_comm` `mul_div_cancel₀` `mul_le_mul_iff_right₀` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Fact.out` `Nat.one_le_cast` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `Mathlib.Tactic.Contrapose.contrapose₄` `zero_div` `MulZeroClass.mul_zero`
`norm_coe_eq_abs_iff` 📖	mathematical	—	`Norm.norm` `HasQuotient.Quotient` `Real` `AddSubgroup` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `QuotientAddGroup.instNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `abs` `Real.lattice` `Real.instAddGroup` `Real.instLE` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `norm_le_half_period` `eq_or_ne` `norm_half_period_eq` `abs_div` `Real.instIsStrictOrderedRing` `Nat.abs_ofNat` `Real.instIsOrderedRing` `round_eq_zero_iff` `abs_le` `Real.instIsOrderedAddMonoid` `Ne.lt_of_le` `le_inv_mul_iff₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `mul_neg` `mul_div_assoc` `mul_one` `inv_mul_lt_iff₀` `norm_eq` `Int.cast_zero` `MulZeroClass.zero_mul` `sub_zero` `Ne.lt_or_gt` `abs_eq_self` `LT.lt.le` `norm_neg_period` `neg_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `abs_eq_neg_self`
`norm_coe_mul` 📖	mathematical	—	`Norm.norm` `HasQuotient.Quotient` `Real` `AddSubgroup` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `Real.instMul` `QuotientAddGroup.instNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `abs` `Real.lattice` `Real.instAddGroup`	—	`eq_or_ne` `AddSubgroup.normal_of_comm` `MulZeroClass.zero_mul` `norm_zero` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `infDist_smul₀` `NormedSpace.toNormSMulClass` `smul_zero` `Set.ext` `zsmul_eq_mul` `mul_left_comm` `Set.range_smul` `Set.mem_smul_set_iff_inv_smul_mem₀` `mul_sub` `inv_mul_cancel_left₀`
`norm_div_natCast` 📖	mathematical	—	`Norm.norm` `HasQuotient.Quotient` `Real` `AddSubgroup` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `QuotientAddGroup.instNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast`	—	`mul_comm` `inv_mul_cancel_left₀` `LT.lt.ne` `Fact.out` `norm_eq'` `abs_sub_round_div_natCast_eq` `Real.instIsStrictOrderedRing`
`norm_eq` 📖	mathematical	—	`Norm.norm` `HasQuotient.Quotient` `Real` `AddSubgroup` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `QuotientAddGroup.instNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `abs` `Real.lattice` `Real.instAddGroup` `Real.instSub` `Real.instMul` `Real.instIntCast` `round` `Real.instRing` `Real.linearOrder` `Real.instFloorRing` `Real.instInv`	—	`le_of_forall_le` `abs_sub_round_eq_min` `Real.instIsStrictOrderedRing` `le_inf_iff` `coe_fract` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `QuotientAddGroup.le_norm_iff` `abs_sub_comm` `Int.abs_one_sub_fract` `AddSubgroup.normal_of_comm` `zsmul_eq_mul` `mul_one` `round_le` `eq_or_ne` `norm_eq_of_zero` `inv_zero` `MulZeroClass.zero_mul` `round_zero` `Int.cast_zero` `MulZeroClass.mul_zero` `sub_zero` `norm_coe_mul` `eq_inv_mul_iff_mul_eq₀` `abs_eq_zero` `covariant_swap_add_of_covariant_add` `abs_inv` `inv_mul_cancel₀` `abs_mul` `Real.instIsOrderedRing` `mul_sub` `mul_inv_cancel_left₀` `mul_comm`
`norm_eq'` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Norm.norm` `HasQuotient.Quotient` `AddSubgroup` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `QuotientAddGroup.instNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instMul` `abs` `Real.lattice` `Real.instAddGroup` `Real.instSub` `Real.instInv` `Real.instIntCast` `round` `Real.instRing` `Real.linearOrder` `Real.instFloorRing`	—	`abs_eq_self` `Real.instIsOrderedAddMonoid` `LT.lt.le` `abs_mul` `Real.instIsOrderedRing` `mul_sub` `mul_inv_cancel_left₀` `LT.lt.ne` `norm_eq` `mul_comm`
`norm_eq_of_zero` 📖	mathematical	—	`Norm.norm` `HasQuotient.Quotient` `Real` `AddSubgroup` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `Real.instZero` `QuotientAddGroup.instNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `abs` `Real.lattice` `Real.instAddGroup`	—	`Set.ext` `AddSubgroup.normal_of_comm` `AddSubgroup.zmultiples_zero_eq_bot` `Metric.infDist_singleton` `dist_zero`
`norm_half_period_eq` 📖	mathematical	—	`Norm.norm` `HasQuotient.Quotient` `Real` `AddSubgroup` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `QuotientAddGroup.instNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `abs` `Real.lattice` `Real.instAddGroup`	—	`Nat.instAtLeastTwoHAddOfNat` `eq_or_ne` `AddSubgroup.normal_of_comm` `zero_div` `norm_zero` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `norm_eq` `mul_div_assoc` `inv_mul_cancel₀` `one_div` `round_two_inv` `Real.instIsStrictOrderedRing` `Int.cast_one` `one_mul` `Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.sub_pf` `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.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `CancelDenoms.sub_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNat_mul` `CancelDenoms.neg_subst` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_lt_true` `abs_neg` `abs_div` `abs_two`
`norm_le_half_period` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `AddCircle` `Real.instAddCommGroup` `QuotientAddGroup.instNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `AddSubgroup.zmultiples` `AddCommGroup.toAddGroup` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `abs` `Real.lattice` `Real.instAddGroup` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `norm_eq` `mul_le_mul_iff_right₀` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `abs_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `inv_ne_zero` `abs_mul` `mul_sub` `mul_left_comm` `mul_div_assoc` `inv_mul_cancel₀` `mul_one` `abs_one` `abs_sub_round`
`norm_neg_period` 📖	mathematical	—	`Norm.norm` `HasQuotient.Quotient` `Real` `AddSubgroup` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `Real.instNeg` `QuotientAddGroup.instNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	—	`norm_coe_mul` `abs_neg` `abs_one` `Real.instIsOrderedRing` `one_mul` `neg_one_mul` `AddSubgroup.normal_of_comm` `neg_mul` `norm_neg`

UnitAddCircle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_eq` 📖	mathematical	—	`Norm.norm` `HasQuotient.Quotient` `Real` `AddSubgroup` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `Real.instOne` `QuotientAddGroup.instNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `abs` `Real.lattice` `Real.instAddGroup` `Real.instSub` `Real.instIntCast` `round` `Real.instRing` `Real.linearOrder` `Real.instFloorRing`	—	`AddCircle.norm_eq` `inv_one` `one_mul` `mul_one`

---

← Back to Index