Mathlib Map

Theorems · Theorem · group theory

mabs_mem_iff

∀ {S : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : LinearOrder G] {x : SetLike S G} [InvMemClass S G] {H : S}
  {x_1 : G}, |x_1|ₘ ∈ H ↔ x_1 ∈ H
Defined in
Mathlib.Algebra.Group.Subgroup.Order
Cited by
1 results in Mathlib
Foundations
Depth 19 from the axioms · uses propext
Assumes
GroupLinearOrderInvMemClass
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Subgroup.exists_isLeast_one_lt · cited by 2Subgroup.exists_isLeast_o…LinearOrder · cited by 8572LinearOrderGroup · cited by 6238GroupSetLike · cited by 1084SetLikemabs · cited by 148mabsInvMemClass · cited by 6InvMemClassmabs_choice · cited by 3mabs_choicemabs_mem_iffCITED BYCITES

Cites6

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

  • LinearOrderstatement and proof · cited by 8,572
  • Groupstatement and proof · cited by 6,238
  • SetLikestatement and proof · cited by 1,084
  • mabsstatement and proof · cited by 148
  • InvMemClassstatement and proof · cited by 6
  • mabs_choiceproof · cited by 3

Cited by1

Results whose statement or proof uses this declaration.