Loogle!

Result

Found 206 declarations mentioning AddCircle. Of these, only the first 200 are shown.

• AddCircle 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) : Type u_1
• AddCircle.liftIco 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] (f : 𝕜 → B) : AddCircle p → B
• AddCircle.liftIoc 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] (f : 𝕜 → B) : AddCircle p → B
• AddCircle.coe_zero 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) : ↑0 = 0
• AddCircle.finite_setOfPred_addOrderOf_eq 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {n : ℕ} (hn : 0 < n) : {u | addOrderOf u = n}.Finite
• AddCircle.finite_setOf_addOrderOf_eq 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {n : ℕ} (hn : 0 < n) : {u | addOrderOf u = n}.Finite
• AddCircle.equivIco 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] : AddCircle p ≃ ↑(Set.Ico a (a + p))
• AddCircle.equivIoc 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] : AddCircle p ≃ ↑(Set.Ioc a (a + p))
• AddCircle.liftIco_comp_apply 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] [Archimedean 𝕜] {α : Type u_3} {β : Type u_4} {f : 𝕜 → α} {g : α → β} {a : 𝕜} {x : AddCircle p} : AddCircle.liftIco p a (g ∘ f) x = g (AddCircle.liftIco p a f x)
• AddCircle.liftIoc_comp_apply 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] [Archimedean 𝕜] {α : Type u_3} {β : Type u_4} {f : 𝕜 → α} {g : α → β} {a : 𝕜} {x : AddCircle p} : AddCircle.liftIoc p a (g ∘ f) x = g (AddCircle.liftIoc p a f x)
• AddCircle.equivIccQuot 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] (p a : 𝕜) [hp : Fact (0 < p)] [Archimedean 𝕜] : AddCircle p ≃ Quot (AddCircle.EndpointIdent p a)
• AddCircle.liftIoc_eq_liftIco_of_ne 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] {a : 𝕜} [Archimedean 𝕜] {f : 𝕜 → B} {x : AddCircle p} (x_ne_a : x ≠ ↑a) : AddCircle.liftIoc p a f x = AddCircle.liftIco p a f x
• AddCircle.liftIoc_eq_liftIco 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p a : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] {f : 𝕜 → B} (hf : f a = f (a + p)) : AddCircle.liftIoc p a f = AddCircle.liftIco p a f
• AddCircle.eq_coe_Ico 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] [Archimedean 𝕜] (a : AddCircle p) : ∃ b ∈ Set.Ico 0 p, ↑b = a
• AddCircle.eq_coe_Ioc 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] [Archimedean 𝕜] (a : AddCircle p) : ∃ b ∈ Set.Ioc 0 p, ↑b = a
• AddCircle.finite_torsion_of_isSMulRegular_int 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) (n : ℤ) (hn : IsSMulRegular 𝕜 n) : {x | n • x = 0}.Finite
• AddCircle.homeomorphAddCircle 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [Field 𝕜] (p q : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (hp : p ≠ 0) (hq : q ≠ 0) : AddCircle p ≃ₜ AddCircle q
• AddCircle.finite_torsion_of_isSMulRegular 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) (n : ℕ) (hn : IsSMulRegular 𝕜 n) : {x | n • x = 0}.Finite
• AddCircle.Ico_ext 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] [Archimedean 𝕜] {α : Type u_3} {f g : AddCircle p → α} (a : 𝕜) (h : ∀ x ∈ Set.Ico a (a + p), f ↑x = g ↑x) : f = g
• AddCircle.Ioc_ext 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] [Archimedean 𝕜] {α : Type u_3} {f g : AddCircle p → α} (a : 𝕜) (h : ∀ x ∈ Set.Ioc a (a + p), f ↑x = g ↑x) : f = g
• AddCircle.card_torsion_le_of_isSMulRegular_int 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) (n : ℤ) (h0 : n ≠ 0) (hn : IsSMulRegular 𝕜 n) : {x | n • x = 0}.encard ≤ ↑n.natAbs
• AddCircle.finite_torsion 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {n : ℕ} (hn : 0 < n) : {u | n • u = 0}.Finite
• AddCircle.openPartialHomeomorphCoe 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] : OpenPartialHomeomorph 𝕜 (AddCircle p)
• AddCircle.card_torsion_le_of_isSMulRegular 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) (n : ℕ) (h0 : n ≠ 0) (hn : IsSMulRegular 𝕜 n) : {x | n • x = 0}.encard ≤ ↑n
• AddCircle.liftIco_continuous 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p a : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [TopologicalSpace B] {f : 𝕜 → B} (hf : f a = f (a + p)) (hc : ContinuousOn f (Set.Icc a (a + p))) : Continuous (AddCircle.liftIco p a f)
• AddCircle.liftIoc_continuous 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p a : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [TopologicalSpace B] {f : 𝕜 → B} (hf : f a = f (a + p)) (hc : ContinuousOn f (Set.Icc a (a + p))) : Continuous (AddCircle.liftIoc p a f)
• AddCircle.card_addOrderOf_eq_totient 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [Field 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {n : ℕ} : Nat.card { u // addOrderOf u = n } = n.totient
• AddCircle.liftIco_zero_continuous 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [TopologicalSpace B] {f : 𝕜 → B} (hf : f 0 = f p) (hc : ContinuousOn f (Set.Icc 0 p)) : Continuous (AddCircle.liftIco p 0 f)
• AddCircle.liftIoc_zero_continuous 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [TopologicalSpace B] {f : 𝕜 → B} (hf : f 0 = f p) (hc : ContinuousOn f (Set.Icc 0 p)) : Continuous (AddCircle.liftIoc p 0 f)
• AddCircle.equivAddCircle 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [Field 𝕜] (p q : 𝕜) (hp : p ≠ 0) (hq : q ≠ 0) : AddCircle p ≃+ AddCircle q
• AddCircle.openPartialHomeomorphCoe_apply 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] (a✝ : 𝕜) : ↑(AddCircle.openPartialHomeomorphCoe p a) a✝ = ↑a✝
• AddCircle.setAddOrderOfEquiv 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [Field 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {n : ℕ} (hn : 0 < n) : ↑{u | addOrderOf u = n} ≃ ↑{m | m < n ∧ m.gcd n = 1}
• AddCircle.homeoIccQuot 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] (p a : 𝕜) [hp : Fact (0 < p)] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] : AddCircle p ≃ₜ Quot (AddCircle.EndpointIdent p a)
• AddCircle.openPartialHomeomorphCoe_source 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] : (AddCircle.openPartialHomeomorphCoe p a).source = Set.Ioo a (a + p)
• AddCircle.openPartialHomeomorphCoe_target 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] : (AddCircle.openPartialHomeomorphCoe p a).target = {↑a}ᶜ
• AddCircle.instDivisibleByInt 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [Field 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] [FloorRing 𝕜] : DivisibleBy (AddCircle p) ℤ
• AddCircle.addOrderOf_eq_pos_iff 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {u : AddCircle p} {n : ℕ} (h : 0 < n) : addOrderOf u = n ↔ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = u
• AddCircle.coe_equivIco 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] {a : 𝕜} [Archimedean 𝕜] {y : AddCircle p} : ↑↑((AddCircle.equivIco p a) y) = y
• AddCircle.coe_equivIoc 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] {a : 𝕜} [Archimedean 𝕜] {y : AddCircle p} : ↑↑((AddCircle.equivIoc p a) y) = y
• AddCircle.equivIco_coe_of_mem 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] {a : 𝕜} [Archimedean 𝕜] {y : 𝕜} (hy : y ∈ Set.Ico a (a + p)) : ↑((AddCircle.equivIco p a) ↑y) = y
• AddCircle.equivIoc_coe_of_mem 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] {a : 𝕜} [Archimedean 𝕜] {y : 𝕜} (hy : y ∈ Set.Ioc a (a + p)) : ↑((AddCircle.equivIoc p a) ↑y) = y
• AddCircle.equivIco_coe_eq 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] {a : 𝕜} [Archimedean 𝕜] {x : 𝕜} (hx : x ∈ Set.Ico a (a + p)) : (AddCircle.equivIco p a) ↑x = ⟨x, hx⟩
• AddCircle.equivIoc_coe_eq 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] {a : 𝕜} [Archimedean 𝕜] {x : 𝕜} (hx : x ∈ Set.Ioc a (a + p)) : (AddCircle.equivIoc p a) ↑x = ⟨x, hx⟩
• AddCircle.continuousAt_equivIco 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {x : AddCircle p} (hx : x ≠ ↑a) : ContinuousAt (⇑(AddCircle.equivIco p a)) x
• AddCircle.continuousAt_equivIoc 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {x : AddCircle p} (hx : x ≠ ↑a) : ContinuousAt (⇑(AddCircle.equivIoc p a)) x
• AddCircle.nsmul_eq_zero_iff 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {u : AddCircle p} {n : ℕ} (h : 0 < n) : n • u = 0 ↔ ∃ m < n, ↑(↑m / ↑n * p) = u
• AddCircle.continuous_equivIco_symm 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] : Continuous ⇑(AddCircle.equivIco p a).symm
• AddCircle.continuous_equivIoc_symm 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] : Continuous ⇑(AddCircle.equivIoc p a).symm
• AddCircle.openPartialHomeomorphCoe_symm_apply 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] (x : AddCircle p) : ↑(AddCircle.openPartialHomeomorphCoe p a).symm x = ↑((AddCircle.equivIco p a) x)
• AddCircle.homeomorphAddCircle_apply_mk 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [Field 𝕜] (p q : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) : (AddCircle.homeomorphAddCircle p q hp hq) ↑x = ↑(x * (p⁻¹ * q))
• AddCircle.liftIco_eq_lift_Icc 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p a : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] {f : 𝕜 → B} (h : f a = f (a + p)) : AddCircle.liftIco p a f = Quot.lift ((Set.Icc a (a + p)).domRestrict f) ⋯ ∘ ⇑(AddCircle.equivIccQuot p a)
• AddCircle.liftIoc_eq_lift_Icc 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p a : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] {f : 𝕜 → B} (h : f a = f (a + p)) : AddCircle.liftIoc p a f = Quot.lift ((Set.Icc a (a + p)).domRestrict f) ⋯ ∘ ⇑(AddCircle.equivIccQuot p a)
• AddCircle.homeomorphAddCircle_symm_apply_mk 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [Field 𝕜] (p q : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) : (AddCircle.homeomorphAddCircle p q hp hq).symm ↑x = ↑(x * (q⁻¹ * p))
• AddCircle.exists_gcd_eq_one_of_isOfFinAddOrder 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {u : AddCircle p} (h : IsOfFinAddOrder u) : ∃ m, m.gcd (addOrderOf u) = 1 ∧ m < addOrderOf u ∧ ↑(↑m / ↑(addOrderOf u) * p) = u
• AddCircle.continuous_equivAddCircle 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [Field 𝕜] (p q : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (hp : p ≠ 0) (hq : q ≠ 0) : Continuous ⇑(AddCircle.equivAddCircle p q hp hq)
• AddCircle.equivIccQuot_comp_mk_eq_toIcoMod 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] (p a : 𝕜) [hp : Fact (0 < p)] [Archimedean 𝕜] : ⇑(AddCircle.equivIccQuot p a) ∘ Quotient.mk'' = fun x => Quot.mk (AddCircle.EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩
• AddCircle.equivIccQuot_comp_mk_eq_toIocMod 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] (p a : 𝕜) [hp : Fact (0 < p)] [Archimedean 𝕜] : ⇑(AddCircle.equivIccQuot p a) ∘ Quotient.mk'' = fun x => Quot.mk (AddCircle.EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩
• AddCircle.equivAddCircle_apply_mk 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [Field 𝕜] (p q : 𝕜) (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) : (AddCircle.equivAddCircle p q hp hq) ↑x = ↑(x * (p⁻¹ * q))
• AddCircle.coe_equivIco_mk_apply 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [Field 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] [FloorRing 𝕜] (x : 𝕜) : ↑((AddCircle.equivIco p 0) ↑x) = Int.fract (x / p) * p
• AddCircle.equivAddCircle_symm_apply_mk 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [Field 𝕜] (p q : 𝕜) (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) : (AddCircle.equivAddCircle p q hp hq).symm ↑x = ↑(x * (q⁻¹ * p))
• AddCircle.equivAddCircle_eq 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [Field 𝕜] (p q : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [hp : Fact (0 < p)] (hq : q ≠ 0) : ⇑(AddCircle.equivAddCircle p q ⋯ hq) = fun x => ↑(↑((AddCircle.equivIco p 0) x) * (p⁻¹ * q))
• CharacterModule.instFunLikeAddCircleRatOfNat 📋 Mathlib.Algebra.Module.CharacterModule
  (A : Type uA) [AddCommGroup A] : FunLike (CharacterModule A) A (AddCircle 1)
• CharacterModule.ext 📋 Mathlib.Algebra.Module.CharacterModule
  (A : Type uA) [AddCommGroup A] {c c' : CharacterModule A} (h : ∀ (x : A), c x = c' x) : c = c'
• CharacterModule.ext_iff 📋 Mathlib.Algebra.Module.CharacterModule
  {A : Type uA} [AddCommGroup A] {c c' : CharacterModule A} : c = c' ↔ ∀ (x : A), c x = c' x
• CharacterModule.instLinearMapClassIntAddCircleRatOfNat 📋 Mathlib.Algebra.Module.CharacterModule
  (A : Type uA) [AddCommGroup A] : LinearMapClass (CharacterModule A) ℤ A (AddCircle 1)
• CharacterModule.int.divByNat_self 📋 Mathlib.Algebra.Module.CharacterModule
  (n : ℕ) : (CharacterModule.int.divByNat n) ↑n = 0
• CharacterModule.eq_zero_of_character_apply 📋 Mathlib.Algebra.Module.CharacterModule
  {A : Type uA} [AddCommGroup A] {a : A} (h : ∀ (c : CharacterModule A), c a = 0) : a = 0
• CharacterModule.exists_character_apply_ne_zero_of_ne_zero 📋 Mathlib.Algebra.Module.CharacterModule
  {A : Type uA} [AddCommGroup A] {a : A} (ne_zero : a ≠ 0) : ∃ c, c a ≠ 0
• CharacterModule.smul_apply 📋 Mathlib.Algebra.Module.CharacterModule
  {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] [Module R A] (c : CharacterModule A) (r : R) (a : A) : (r • c) a = c (r • a)
• CharacterModule.dual_apply 📋 Mathlib.Algebra.Module.CharacterModule
  {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] (f : A →ₗ[R] B) (L : CharacterModule B) : (CharacterModule.dual f) L = AddMonoidHom.comp L f.toAddMonoidHom
• CharacterModule.eq_zero_of_ofSpanSingleton_apply_self 📋 Mathlib.Algebra.Module.CharacterModule
  {A : Type uA} [AddCommGroup A] (a : A) (h : (CharacterModule.ofSpanSingleton a) ⟨a, ⋯⟩ = 0) : a = 0
• CharacterModule.uncurry_apply 📋 Mathlib.Algebra.Module.CharacterModule
  {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] (c : A →ₗ[R] CharacterModule B) : CharacterModule.uncurry c = TensorProduct.liftAddHom c.toAddMonoidHom ⋯
• CharacterModule.curry_apply_apply 📋 Mathlib.Algebra.Module.CharacterModule
  {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] (c : CharacterModule (TensorProduct R A B)) (x✝ : A) : (CharacterModule.curry c) x✝ = AddMonoidHom.comp c ↑((TensorProduct.mk R A B) x✝)
• CharacterModule.homEquiv_symm_apply_apply_apply 📋 Mathlib.Algebra.Module.CharacterModule
  {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] (a : CharacterModule (TensorProduct R A B)) (x✝ : A) (x : B) : ((CharacterModule.homEquiv.symm a) x✝) x = a (x✝ ⊗ₜ[R] x)
• CharacterModule.homEquiv_apply_apply 📋 Mathlib.Algebra.Module.CharacterModule
  {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] (c : A →ₗ[R] CharacterModule B) (x : (addConGen (TensorProduct.Eqv R A B)).Quotient) : (CharacterModule.homEquiv c) x = AddCon.liftOn x ⇑(FreeAddMonoid.lift fun mn => (c.toAddMonoidHom mn.1) mn.2) ⋯
• AddCircle.pathConnectedSpace 📋 Mathlib.Topology.Instances.AddCircle.Real
  (p : ℝ) : PathConnectedSpace (AddCircle p)
• AddCircle.compactSpace 📋 Mathlib.Topology.Instances.AddCircle.Real
  (p : ℝ) [Fact (0 < p)] : CompactSpace (AddCircle p)
• AddCircle.instNormedAddCommGroupReal 📋 Mathlib.Analysis.Normed.Group.AddCircle
  (p : ℝ) : NormedAddCommGroup (AddCircle p)
• AddCircle.norm_le_half_period 📋 Mathlib.Analysis.Normed.Group.AddCircle
  (p : ℝ) {x : AddCircle p} (hp : p ≠ 0) : ‖x‖ ≤ |p| / 2
• AddCircle.closedBall_eq_univ_of_half_period_le 📋 Mathlib.Analysis.Normed.Group.AddCircle
  (p : ℝ) (hp : p ≠ 0) (x : AddCircle p) {ε : ℝ} (hε : |p| / 2 ≤ ε) : Metric.closedBall x ε = Set.univ
• AddCircle.exists_norm_eq_of_isOfFinAddOrder 📋 Mathlib.Analysis.Normed.Group.AddCircle
  {p : ℝ} [hp : Fact (0 < p)] {u : AddCircle p} (hu : IsOfFinAddOrder u) : ∃ k, ‖u‖ = p * (↑k / ↑(addOrderOf u))
• AddCircle.le_add_order_smul_norm_of_isOfFinAddOrder 📋 Mathlib.Analysis.Normed.Group.AddCircle
  {p : ℝ} [hp : Fact (0 < p)] {u : AddCircle p} (hu : IsOfFinAddOrder u) (hu' : u ≠ 0) : p ≤ addOrderOf u • ‖u‖
• AddCircle.measureSpace 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  (T : ℝ) [hT : Fact (0 < T)] : MeasureTheory.MeasureSpace (AddCircle T)
• AddCircle.measurable_mk' 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  {a : ℝ} : Measurable QuotientAddGroup.mk
• AddCircle.isFiniteMeasure 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  (T : ℝ) [hT : Fact (0 < T)] : MeasureTheory.IsFiniteMeasure MeasureTheory.volume
• AddCircle.instIsUnifLocDoublingMeasureRealVolume 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  (T : ℝ) [hT : Fact (0 < T)] : IsUnifLocDoublingMeasure MeasureTheory.volume
• AddCircle.measure_univ 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  (T : ℝ) [hT : Fact (0 < T)] : MeasureTheory.volume Set.univ = ENNReal.ofReal T
• AddCircle.measurableEquivIco 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  (T : ℝ) [hT : Fact (0 < T)] (a : ℝ) : AddCircle T ≃ᵐ ↑(Set.Ico a (a + T))
• AddCircle.measurableEquivIoc 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  (T : ℝ) [hT : Fact (0 < T)] (a : ℝ) : AddCircle T ≃ᵐ ↑(Set.Ioc a (a + T))
• AddCircle.measurePreserving_mk 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  (T : ℝ) [hT : Fact (0 < T)] (t : ℝ) : MeasureTheory.MeasurePreserving QuotientAddGroup.mk (MeasureTheory.volume.restrict (Set.Ioc t (t + T))) MeasureTheory.volume
• AddCircle.instIsAddHaarMeasureRealVolume 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  (T : ℝ) [hT : Fact (0 < T)] : MeasureTheory.volume.IsAddHaarMeasure
• AddCircle.integral_liftIoc_eq_intervalIntegral 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  (T : ℝ) [hT : Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {t : ℝ} {f : ℝ → E} : ∫ (a : AddCircle T), AddCircle.liftIoc T t f a = ∫ (a : ℝ) in t..t + T, f a
• AddCircle.lintegral_preimage 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  (T : ℝ) [hT : Fact (0 < T)] (t : ℝ) (f : AddCircle T → ENNReal) : ∫⁻ (a : ℝ) in Set.Ioc t (t + T), f ↑a = ∫⁻ (b : AddCircle T), f b
• AddCircle.intervalIntegral_preimage 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  (T : ℝ) [hT : Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (t : ℝ) (f : AddCircle T → E) : ∫ (a : ℝ) in t..t + T, f ↑a = ∫ (b : AddCircle T), f b
• AddCircle.integral_preimage 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  (T : ℝ) [hT : Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (t : ℝ) (f : AddCircle T → E) : ∫ (a : ℝ) in Set.Ioc t (t + T), f ↑a = ∫ (b : AddCircle T), f b
• AddCircle.volume_closedBall 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  (T : ℝ) [hT : Fact (0 < T)] {x : AddCircle T} (ε : ℝ) : MeasureTheory.volume (Metric.closedBall x ε) = ENNReal.ofReal (min T (2 * ε))
• AddCircle.instAddQuotientMeasureEqMeasurePreimageSubtypeAddOppositeRealMemAddSubgroupOpZmultiplesVolume 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  (T : ℝ) [hT : Fact (0 < T)] : MeasureTheory.AddQuotientMeasureEqMeasurePreimage MeasureTheory.volume MeasureTheory.volume
• AddCircle.add_projection_respects_measure 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  (T : ℝ) [hT : Fact (0 < T)] (t : ℝ) {U : Set (AddCircle T)} (meas_U : MeasurableSet U) : MeasureTheory.volume U = MeasureTheory.volume (QuotientAddGroup.mk ⁻¹' U ∩ Set.Ioc t (t + T))
• MeasureTheory.MemLp.memLp_liftIoc 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  {T : ℝ} [hT : Fact (0 < T)] {t : ℝ} {f : ℝ → ℂ} {p : ENNReal} (hLp : MeasureTheory.MemLp f p (MeasureTheory.volume.restrict (Set.Ioc t (t + T)))) : MeasureTheory.MemLp (AddCircle.liftIoc T t f) p MeasureTheory.volume
• AddCircle.measurePreserving_equivIoc 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  (T : ℝ) [hT : Fact (0 < T)] {a : ℝ} : MeasureTheory.MeasurePreserving (⇑(AddCircle.equivIoc T a)) MeasureTheory.volume (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)
• AddCircle.isAddQuotientCoveringMap_zsmul 📋 Mathlib.Topology.Covering.AddCircle
  {𝕜 : Type u_1} [TopologicalSpace 𝕜] [Ring 𝕜] [IsTopologicalRing 𝕜] (p : 𝕜) [T0Space (AddCircle p)] {n : ℤ} (hn : IsUnit ↑n) : IsAddQuotientCoveringMap (fun x => n • x) ↥(zsmulAddGroupHom n).ker
• AddCircle.isAddQuotientCoveringMap_zsmul_of_ne_zero 📋 Mathlib.Topology.Covering.AddCircle
  {𝕜 : Type u_1} [TopologicalSpace 𝕜] [Ring 𝕜] [IsTopologicalRing 𝕜] (p : 𝕜) [T0Space (AddCircle p)] [Algebra ℚ 𝕜] (n : ℤ) [NeZero n] : IsAddQuotientCoveringMap (fun x => n • x) ↥(zsmulAddGroupHom n).ker
• AddCircle.isAddQuotientCoveringMap_nsmul_of_ne_zero 📋 Mathlib.Topology.Covering.AddCircle
  {𝕜 : Type u_1} [TopologicalSpace 𝕜] [Ring 𝕜] [IsTopologicalRing 𝕜] (p : 𝕜) [T0Space (AddCircle p)] [Algebra ℚ 𝕜] (n : ℕ) [NeZero n] : IsAddQuotientCoveringMap (fun x => n • x) ↥(nsmulAddMonoidHom n).ker
• AddCircle.isAddQuotientCoveringMap_nsmul 📋 Mathlib.Topology.Covering.AddCircle
  {𝕜 : Type u_1} [TopologicalSpace 𝕜] [Ring 𝕜] [IsTopologicalRing 𝕜] (p : 𝕜) [T0Space (AddCircle p)] {n : ℕ} (hn : IsUnit ↑n) : IsAddQuotientCoveringMap (fun x => n • x) ↥(nsmulAddMonoidHom n).ker
• AddCircle.toCircle 📋 Mathlib.Analysis.SpecialFunctions.Complex.Circle
  {T : ℝ} : AddCircle T → Circle
• AddCircle.injective_toCircle 📋 Mathlib.Analysis.SpecialFunctions.Complex.Circle
  {T : ℝ} (hT : T ≠ 0) : Function.Injective AddCircle.toCircle
• AddCircle.continuous_toCircle 📋 Mathlib.Analysis.SpecialFunctions.Complex.Circle
  {T : ℝ} : Continuous AddCircle.toCircle
• AddCircle.homeomorphCircle 📋 Mathlib.Analysis.SpecialFunctions.Complex.Circle
  {T : ℝ} (hT : T ≠ 0) : AddCircle T ≃ₜ Circle
• AddCircle.toCircle_neg 📋 Mathlib.Analysis.SpecialFunctions.Complex.Circle
  {T : ℝ} (x : AddCircle T) : (-x).toCircle = x.toCircle⁻¹
• AddCircle.toCircle_zero 📋 Mathlib.Analysis.SpecialFunctions.Complex.Circle
  {T : ℝ} : AddCircle.toCircle 0 = 1
• AddCircle.homeomorphCircle' 📋 Mathlib.Analysis.SpecialFunctions.Complex.Circle
  : AddCircle (2 * Real.pi) ≃ₜ Circle
• AddCircle.toCircle_add 📋 Mathlib.Analysis.SpecialFunctions.Complex.Circle
  {T : ℝ} (x y : AddCircle T) : (x + y).toCircle = x.toCircle * y.toCircle
• AddCircle.toCircle_zsmul 📋 Mathlib.Analysis.SpecialFunctions.Complex.Circle
  {T : ℝ} (x : AddCircle T) (n : ℤ) : (n • x).toCircle = x.toCircle ^ n
• AddCircle.toCircle_nsmul 📋 Mathlib.Analysis.SpecialFunctions.Complex.Circle
  {T : ℝ} (x : AddCircle T) (n : ℕ) : (n • x).toCircle = x.toCircle ^ n
• AddCircle.homeomorphCircle_apply 📋 Mathlib.Analysis.SpecialFunctions.Complex.Circle
  {T : ℝ} (hT : T ≠ 0) (x : AddCircle T) : (AddCircle.homeomorphCircle hT) x = x.toCircle
• AddCircle.homeomorphCircle'_apply 📋 Mathlib.Analysis.SpecialFunctions.Complex.Circle
  (θ : Real.Angle) : AddCircle.homeomorphCircle' θ = θ.toCircle
• AddCircle.homeomorphCircle'_apply_mk 📋 Mathlib.Analysis.SpecialFunctions.Complex.Circle
  (x : ℝ) : AddCircle.homeomorphCircle' ↑x = Circle.exp x
• AddCircle.homeomorphCircle'_symm_apply 📋 Mathlib.Analysis.SpecialFunctions.Complex.Circle
  (x : Circle) : AddCircle.homeomorphCircle'.symm x = ↑(↑x).arg
• fourierCoeff 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : AddCircle T → E) (n : ℤ) : E
• AddCircle.haarAddCircle 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] : MeasureTheory.Measure (AddCircle T)
• AddCircle.instIsProbabilityMeasureRealHaarAddCircle 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] : MeasureTheory.IsProbabilityMeasure AddCircle.haarAddCircle
• fourier 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} (n : ℤ) : C(AddCircle T, ℂ)
• AddCircle.instIsAddHaarMeasureRealHaarAddCircle 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] : AddCircle.haarAddCircle.IsAddHaarMeasure
• fourierCoeff.const_mul 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] (f : AddCircle T → ℂ) (c : ℂ) (n : ℤ) : fourierCoeff (fun x => c * f x) n = c * fourierCoeff f n
• fourier_norm 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [Fact (0 < T)] (n : ℤ) : ‖fourier n‖ = 1
• fourier_zero 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} {x : AddCircle T} : (fourier 0) x = 1
• fourierCoeff_congr_ae 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : AddCircle T → E} (h : f =ᵐ[AddCircle.haarAddCircle] g) : fourierCoeff f = fourierCoeff g
• fourier_zero' 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} : ↑(AddCircle.toCircle 0) = 1
• fourierCoeff_fourier 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] (n : ℤ) : fourierCoeff ⇑(fourier n) = Pi.single n 1
• AddCircle.volume_eq_smul_haarAddCircle 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] : MeasureTheory.volume = ENNReal.ofReal T • AddCircle.haarAddCircle
• fourier_eval_zero 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} (n : ℤ) : (fourier n) 0 = 1
• fourierCoeff.sum 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {ι : Type u_2} (s : Finset ι) (f : ι → AddCircle T → E) (hf : ∀ i ∈ s, MeasureTheory.Integrable (f i) AddCircle.haarAddCircle) : fourierCoeff (∑ i ∈ s, f i) = ∑ i ∈ s, fourierCoeff (f i)
• AddCircle.integral_haarAddCircle 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : AddCircle T → E} : ∫ (t : AddCircle T), f t ∂AddCircle.haarAddCircle = T⁻¹ • ∫ (t : AddCircle T), f t
• MeasureTheory.MemLp.haarAddCircle 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] {f : AddCircle T → ℂ} {p : ENNReal} : MeasureTheory.MemLp f p MeasureTheory.volume → MeasureTheory.MemLp f p AddCircle.haarAddCircle
• MeasureTheory.MemLp.of_haarAddCircle 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] {f : AddCircle T → ℂ} {p : ENNReal} : MeasureTheory.MemLp f p AddCircle.haarAddCircle → MeasureTheory.MemLp f p MeasureTheory.volume
• MeasureTheory.memLp_haarAddCircle_iff 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] {f : AddCircle T → ℂ} {p : ENNReal} : MeasureTheory.MemLp f p AddCircle.haarAddCircle ↔ MeasureTheory.MemLp f p MeasureTheory.volume
• fourier_coe_apply 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} {n : ℤ} {x : ℝ} : (fourier n) ↑x = Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * ↑x / ↑T)
• fourier_one 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} {x : AddCircle T} : (fourier 1) x = ↑x.toCircle
• fourierCoeff.add 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : AddCircle T → E} (hf : MeasureTheory.Integrable f AddCircle.haarAddCircle) (hg : MeasureTheory.Integrable g AddCircle.haarAddCircle) : fourierCoeff (f + g) = fourierCoeff f + fourierCoeff g
• fourierCoeff.const_smul 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : AddCircle T → E) (c : ℂ) (n : ℤ) : fourierCoeff (c • f) n = c • fourierCoeff f n
• fourier_neg 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} {n : ℤ} {x : AddCircle T} : (fourier (-n)) x = (starRingEnd ℂ) ((fourier n) x)
• fourier_apply 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} {n : ℤ} {x : AddCircle T} : (fourier n) x = ↑(n • x).toCircle
• MeasureTheory.Integrable.fourier_smul 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : AddCircle T → E} (hf : MeasureTheory.Integrable f AddCircle.haarAddCircle) (n : ℤ) : MeasureTheory.Integrable (fun t => (fourier n) t • f t) AddCircle.haarAddCircle
• fourier_add 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} {m n : ℤ} {x : AddCircle T} : (fourier (m + n)) x = (fourier m) x * (fourier n) x
• fourier_add_half_inv_index 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} {n : ℤ} (hn : n ≠ 0) (hT : 0 < T) (x : AddCircle T) : (fourier n) (x + ↑(T / 2 / ↑n)) = -(fourier n) x
• fourier_neg' 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} {n : ℤ} {x : AddCircle T} : ↑(-(n • x)).toCircle = (starRingEnd ℂ) ((fourier n) x)
• fourier_add' 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} {m n : ℤ} {x : AddCircle T} : ↑((m + n) • x).toCircle = (fourier m) x * (fourier n) x
• fourierCoeff_eq_intervalIntegral 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : AddCircle T → E) (n : ℤ) (a : ℝ) : fourierCoeff f n = (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f ↑x
• fourierCoeffOn_eq_integral 📋 Mathlib.Analysis.Fourier.AddCircle
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b : ℝ} (f : ℝ → E) (n : ℤ) (hab : a < b) : fourierCoeffOn hab f n = (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x
• fourierLp 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] (p : ENNReal) [Fact (1 ≤ p)] (n : ℤ) : ↥(MeasureTheory.Lp ℂ p AddCircle.haarAddCircle)
• hasDerivAt_fourier 📋 Mathlib.Analysis.Fourier.AddCircle
  (T : ℝ) (n : ℤ) (x : ℝ) : HasDerivAt (fun y => (fourier n) ↑y) (2 * ↑Real.pi * Complex.I * ↑n / ↑T * (fourier n) ↑x) x
• hasDerivAt_fourier_neg 📋 Mathlib.Analysis.Fourier.AddCircle
  (T : ℝ) (n : ℤ) (x : ℝ) : HasDerivAt (fun y => (fourier (-n)) ↑y) (-2 * ↑Real.pi * Complex.I * ↑n / ↑T * (fourier (-n)) ↑x) x
• has_antideriv_at_fourier_neg 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} (hT : Fact (0 < T)) {n : ℤ} (hn : n ≠ 0) (x : ℝ) : HasDerivAt (fun y => ↑T / (-2 * ↑Real.pi * Complex.I * ↑n) * (fourier (-n)) ↑y) ((fourier (-n)) ↑x) x
• has_pointwise_sum_fourier_series_of_summable 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] {f : C(AddCircle T, ℂ)} (h : Summable (fourierCoeff ⇑f)) (x : AddCircle T) : HasSum (fun i => fourierCoeff (⇑f) i • (fourier i) x) (f x)
• fourierSubalgebra 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} : StarSubalgebra ℂ C(AddCircle T, ℂ)
• fourierBasis 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] : HilbertBasis ℤ ℂ ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)
• fourierCoeffOn_of_hasDerivAt 📋 Mathlib.Analysis.Fourier.AddCircle
  {a b : ℝ} (hab : a < b) {f f' : ℝ → ℂ} {n : ℤ} (hn : n ≠ 0) (hf : ∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) (hf' : IntervalIntegrable f' MeasureTheory.volume a b) : fourierCoeffOn hab f n = 1 / (-2 * ↑Real.pi * Complex.I * ↑n) * ((fourier (-n)) ↑a * (f b - f a) - (↑b - ↑a) * fourierCoeffOn hab f' n)
• fourierCoeffOn_of_hasDerivAt_Ioo 📋 Mathlib.Analysis.Fourier.AddCircle
  {a b : ℝ} (hab : a < b) {f f' : ℝ → ℂ} {n : ℤ} (hn : n ≠ 0) (hf : ContinuousOn f (Set.uIcc a b)) (hff' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt f (f' x) x) (hf' : IntervalIntegrable f' MeasureTheory.volume a b) : fourierCoeffOn hab f n = 1 / (-2 * ↑Real.pi * Complex.I * ↑n) * ((fourier (-n)) ↑a * (f b - f a) - (↑b - ↑a) * fourierCoeffOn hab f' n)
• fourierCoeffOn_of_hasDeriv_right 📋 Mathlib.Analysis.Fourier.AddCircle
  {a b : ℝ} (hab : a < b) {f f' : ℝ → ℂ} {n : ℤ} (hn : n ≠ 0) (hf : ContinuousOn f (Set.uIcc a b)) (hff' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) (hf' : IntervalIntegrable f' MeasureTheory.volume a b) : fourierCoeffOn hab f n = 1 / (-2 * ↑Real.pi * Complex.I * ↑n) * ((fourier (-n)) ↑a * (f b - f a) - (↑b - ↑a) * fourierCoeffOn hab f' n)
• fourierSubalgebra_separatesPoints 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] : fourierSubalgebra.SeparatesPoints
• coeFn_fourierLp 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] (p : ENNReal) [Fact (1 ≤ p)] (n : ℤ) : ↑↑(fourierLp p n) =ᵐ[AddCircle.haarAddCircle] ⇑(fourier n)
• hasSum_fourier_series_of_summable 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] {f : C(AddCircle T, ℂ)} (h : Summable (fourierCoeff ⇑f)) : HasSum (fun i => fourierCoeff (⇑f) i • fourier i) f
• orthonormal_fourier 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] : Orthonormal ℂ (fourierLp 2)
• hasSum_sq_fourierCoeff 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) : HasSum (fun i => ‖fourierCoeff (↑↑f) i‖ ^ 2) (∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂AddCircle.haarAddCircle)
• tsum_sq_fourierCoeff 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) : ∑' (i : ℤ), ‖fourierCoeff (↑↑f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂AddCircle.haarAddCircle
• coe_fourierBasis 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] : ⇑fourierBasis = fourierLp 2
• span_fourier_closure_eq_top 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] : (Submodule.span ℂ (Set.range fourier)).topologicalClosure = ⊤
• fourierSubalgebra_coe 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} : Subalgebra.toSubmodule fourierSubalgebra.toSubalgebra = Submodule.span ℂ (Set.range fourier)
• fourierCoeff_toLp 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] (f : C(AddCircle T, ℂ)) (n : ℤ) : fourierCoeff (↑↑((ContinuousMap.toLp 2 AddCircle.haarAddCircle ℂ) f)) n = fourierCoeff (⇑f) n
• fourierSubalgebra_closure_eq_top 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] : fourierSubalgebra.topologicalClosure = ⊤
• hasSum_fourier_series_L2 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) : HasSum (fun i => fourierCoeff (↑↑f) i • fourierLp 2 i) f
• fourierBasis_repr 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) (i : ℤ) : ↑(fourierBasis.repr f) i = fourierCoeff (↑↑f) i
• span_fourierLp_closure_eq_top 📋 Mathlib.Analysis.Fourier.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) : (Submodule.span ℂ (Set.range (fourierLp p))).topologicalClosure = ⊤
• UnitAddTorus.mFourier_single 📋 Mathlib.Analysis.Fourier.AddCircleMulti
  {d : Type u_1} [Fintype d] [DecidableEq d] (z : d → AddCircle 1) (i : d) : (UnitAddTorus.mFourier (Pi.single i 1)) z = (fourier 1) (z i)
• UnitAddTorus.coe_measurableEquivPiIoc_apply 📋 Mathlib.Analysis.Fourier.AddCircleMulti
  {ι : Type u_2} (b : ι → ℝ) (x : UnitAddTorus ι) : (UnitAddTorus.measurableEquivPiIoc b) x = ⟨fun i => ↑((AddCircle.equivIoc 1 (b i)) (x i)), ⋯⟩
• UnitAddTorus.coe_measurableEquivPiIoc 📋 Mathlib.Analysis.Fourier.AddCircleMulti
  {ι : Type u_2} (b : ι → ℝ) : ⇑(UnitAddTorus.measurableEquivPiIoc b) = fun x => ⟨fun i => ↑((AddCircle.equivIoc 1 (b i)) (x i)), ⋯⟩
• Real.tsum_eq_tsum_fourier_of_rpow_decay_of_summable 📋 Mathlib.Analysis.Fourier.PoissonSummation
  {f : ℝ → ℂ} (hc : Continuous f) {b : ℝ} (hb : 1 < b) (hf : f =O[Filter.cocompact ℝ] fun x => |x| ^ (-b)) (hFf : Summable fun n => FourierTransform.fourier f ↑n) (x : ℝ) : ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), FourierTransform.fourier f ↑n * (fourier n) ↑x
• Real.tsum_eq_tsum_fourier_of_rpow_decay 📋 Mathlib.Analysis.Fourier.PoissonSummation
  {f : ℝ → ℂ} (hc : Continuous f) {b : ℝ} (hb : 1 < b) (hf : f =O[Filter.cocompact ℝ] fun x => |x| ^ (-b)) (hFf : FourierTransform.fourier f =O[Filter.cocompact ℝ] fun x => |x| ^ (-b)) (x : ℝ) : ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), FourierTransform.fourier f ↑n * (fourier n) ↑x
• SchwartzMap.tsum_eq_tsum_fourier 📋 Mathlib.Analysis.Fourier.PoissonSummation
  (f : SchwartzMap ℝ ℂ) (x : ℝ) : ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), (FourierTransform.fourier f) ↑n * (fourier n) ↑x
• Real.tsum_eq_tsum_fourier 📋 Mathlib.Analysis.Fourier.PoissonSummation
  {f : C(ℝ, ℂ)} (h_norm : ∀ (K : TopologicalSpace.Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖) (h_sum : Summable fun n => FourierTransform.fourier ⇑f ↑n) (x : ℝ) : ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), FourierTransform.fourier ⇑f ↑n * (fourier n) ↑x
• AddCircle.toCircle_addChar 📋 Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
  {T : ℝ} : AddChar (AddCircle T) Circle
• Polynomial.toAddCircle 📋 Mathlib.Analysis.Polynomial.Fourier
  : Polynomial ℂ →ₐ[ℂ] C(AddCircle (2 * Real.pi), ℂ)
• Polynomial.toAddCircle_X_eq_fourier_one 📋 Mathlib.Analysis.Polynomial.Fourier
  : Polynomial.toAddCircle Polynomial.X = fourier 1
• Polynomial.toAddCircle_X_pow_eq_fourier 📋 Mathlib.Analysis.Polynomial.Fourier
  {n : ℕ} : Polynomial.toAddCircle (Polynomial.X ^ n) = fourier ↑n
• Polynomial.fourierCoeff_toAddCircle_natCast 📋 Mathlib.Analysis.Polynomial.Fourier
  (p : Polynomial ℂ) (n : ℕ) : fourierCoeff ⇑(Polynomial.toAddCircle p) ↑n = p.coeff n
• Polynomial.fourierCoeff_toAddCircle_eq_zero_of_lt_zero 📋 Mathlib.Analysis.Polynomial.Fourier
  (p : Polynomial ℂ) (n : ℤ) (hn : n < 0) : fourierCoeff (⇑(Polynomial.toAddCircle p)) n = 0
• Polynomial.fourierCoeff_toAddCircle 📋 Mathlib.Analysis.Polynomial.Fourier
  (p : Polynomial ℂ) (n : ℤ) : fourierCoeff (⇑(Polynomial.toAddCircle p)) n = if 0 ≤ n then p.coeff n.natAbs else 0
• Polynomial.toAddCircle.integrable 📋 Mathlib.Analysis.Polynomial.Fourier
  (p : Polynomial ℂ) : MeasureTheory.Integrable (⇑(Polynomial.toAddCircle p)) AddCircle.haarAddCircle
• Polynomial.toAddCircle_C_eq_smul_fourier_zero 📋 Mathlib.Analysis.Polynomial.Fourier
  {c : ℂ} : Polynomial.toAddCircle (Polynomial.C c) = c • fourier 0
• Polynomial.toAddCircle_monomial_eq_smul_fourier 📋 Mathlib.Analysis.Polynomial.Fourier
  {n : ℕ} {c : ℂ} : Polynomial.toAddCircle ((Polynomial.monomial n) c) = c • fourier ↑n
• AddCircle.closedBall_ae_eq_ball 📋 Mathlib.MeasureTheory.Group.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] {x : AddCircle T} {ε : ℝ} : Metric.closedBall x ε =ᵐ[MeasureTheory.volume] Metric.ball x ε
• AddCircle.volume_of_add_preimage_eq 📋 Mathlib.MeasureTheory.Group.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] (s I : Set (AddCircle T)) (u x : AddCircle T) (hu : IsOfFinAddOrder u) (hs : u +ᵥ s =ᵐ[MeasureTheory.volume] s) (hI : I =ᵐ[MeasureTheory.volume] Metric.ball x (T / (2 * ↑(addOrderOf u)))) : MeasureTheory.volume s = addOrderOf u • MeasureTheory.volume (s ∩ I)
• AddCircle.isAddFundamentalDomain_of_ae_ball 📋 Mathlib.MeasureTheory.Group.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] (I : Set (AddCircle T)) (u x : AddCircle T) (hu : IsOfFinAddOrder u) (hI : I =ᵐ[MeasureTheory.volume] Metric.ball x (T / (2 * ↑(addOrderOf u)))) : MeasureTheory.IsAddFundamentalDomain (↥(AddSubgroup.zmultiples u)) I MeasureTheory.volume
• AddCircle.ergodic_zsmul 📋 Mathlib.Dynamics.Ergodic.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] {n : ℤ} (hn : 1 < |n|) : Ergodic (fun y => n • y) MeasureTheory.volume
• AddCircle.ergodic_nsmul 📋 Mathlib.Dynamics.Ergodic.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] {n : ℕ} (hn : 1 < n) : Ergodic (fun y => n • y) MeasureTheory.volume
• AddCircle.ergodic_zsmul_add 📋 Mathlib.Dynamics.Ergodic.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] (x : AddCircle T) {n : ℤ} (h : 1 < |n|) : Ergodic (fun y => n • y + x) MeasureTheory.volume
• AddCircle.ergodic_nsmul_add 📋 Mathlib.Dynamics.Ergodic.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] (x : AddCircle T) {n : ℕ} (h : 1 < n) : Ergodic (fun y => n • y + x) MeasureTheory.volume
• AddCircle.ae_empty_or_univ_of_forall_vadd_ae_eq_self 📋 Mathlib.Dynamics.Ergodic.AddCircle
  {T : ℝ} [hT : Fact (0 < T)] {s : Set (AddCircle T)} (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) {ι : Type u_1} {l : Filter ι} [l.NeBot] {u : ι → AddCircle T} (hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[MeasureTheory.volume] s) (hu₂ : Filter.Tendsto (addOrderOf ∘ u) l Filter.atTop) : s =ᵐ[MeasureTheory.volume] ∅ ∨ s =ᵐ[MeasureTheory.volume] Set.univ
• AddCircle.denseRange_zsmul_iff 📋 Mathlib.Topology.Instances.AddCircle.DenseSubgroup
  {p : ℝ} [Fact (0 < p)] {a : AddCircle p} : (DenseRange fun x => x • a) ↔ addOrderOf a = 0
• AddCircle.dense_addSubgroup_iff_ne_zmultiples 📋 Mathlib.Topology.Instances.AddCircle.DenseSubgroup
  {p : ℝ} [Fact (0 < p)] {s : AddSubgroup (AddCircle p)} : Dense ↑s ↔ ∀ (a : AddCircle p), addOrderOf a ≠ 0 → s ≠ AddSubgroup.zmultiples a

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59