Mathlib Map

Theorems · Theorem · number theory

IsApproximateSubgroup.one_mem

∀ {G : Type u_1} [inst : Group G] {K : ℝ} {A : Set G}, IsApproximateSubgroup K A → 1 ∈ A
Defined in
Mathlib.Combinatorics.Additive.ApproximateSubgroup
Cited by
5 results in Mathlib
Foundations
Depth 12 from the axioms · uses propext
Assumes
Group
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

IsApproximateSubgroup.nonempty · cited by 3IsApproximateSubgroup.non…isApproximateSubgroup_one · cited by 0isApproximateSubgroup_oneIsApproximateSubgroup.image · cited by 0IsApproximateSubgroup.ima…IsApproximateSubgroup.mono · cited by 0IsApproximateSubgroup.monoIsApproximateSubgroup.pow_inter_pow · cited by 0IsApproximateSubgroup.pow…Set · cited by 53352SetReal · cited by 25697RealGroup · cited by 6238GroupIsApproximateSubgroup · cited by 14IsApproximateSubgroupIsApproximateSubgroup.one_memCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement and proof · cited by 53,352
  • Realstatement and proof · cited by 25,697
  • Groupstatement and proof · cited by 6,238
  • IsApproximateSubgroupstatement and proof · cited by 14

Cited by5

Results whose statement or proof uses this declaration.