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	13 math math: toCircle_add, isAddFundamentalDomain_of_ae_ball, ergodic_nsmul_add, exists_norm_nsmul_le, ergodic_add_left, ergodic_add_right, volume_of_add_preimage_eq, exists_norm_eq_of_isOfFinAddOrder, ergodic_nsmul, le_add_order_smul_norm_of_isOfFinAddOrder, 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 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 Real Set.instInter Set.preimage 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 Real.instLT DivInvMonoid.toDiv Real.instDivInvMonoid abs Real.lattice Real.instAddGroup instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.decidableLT Real.pseudoMetricSpace	—	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 instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid 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 Mathlib.Tactic.CancelDenoms.sub_subst Mathlib.Tactic.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 Mathlib.Tactic.CancelDenoms.add_subst Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.add_nonpos Mathlib.Tactic.Linarith.without_one_mul Mathlib.Tactic.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 AddCircle Real Real.instAddCommGroup 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 ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroupReal ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	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 Real.instLE AddMonoid.toNSMul Real.instAddMonoid addOrderOf AddCircle 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	—	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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid 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 Real 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 Mathlib.Tactic.CancelDenoms.sub_subst Mathlib.Tactic.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.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