Mathlib Map

Theorems · Theorem · order theory

mabs_div_comm

∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] (a b : α), |a / b|ₘ = |b / a|ₘ
Defined in
Mathlib.Algebra.Order.Group.Unbundled.Abs
Cited by
8 results in Mathlib
Foundations
Depth 14 from the axioms · uses propext
Assumes
LatticeGroup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

nhds_basis_mabs_div_lt · cited by 2nhds_basis_mabs_div_ltLinearOrderedCommGroup.tendsto_nhds · cited by 0LinearOrderedCommGroup.te…eventually_mabs_div_lt · cited by 0eventually_mabs_div_ltmax_div_min_eq_mabs · cited by 0max_div_min_eq_mabsdiv_le_of_mabs_div_le_right · cited by 0div_le_of_mabs_div_le_rig…div_lt_of_mabs_div_lt_right · cited by 0div_lt_of_mabs_div_lt_rig…mabs_mabs_div_mabs_le · cited by 0mabs_mabs_div_mabs_lemabs_mabs_div_mabs_le_mabs_div · cited by 0mabs_mabs_div_mabs_le_mab…Group · cited by 6238GroupLattice · cited by 916Latticemabs · cited by 148mabsinv_div · cited by 92inv_divmabs_inv · cited by 13mabs_invmabs_div_commCITED BYCITES

Cites5

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

  • Groupstatement and proof · cited by 6,238
  • Latticestatement and proof · cited by 916
  • mabsstatement and proof · cited by 148
  • inv_divproof · cited by 92
  • mabs_invproof · cited by 13

Cited by8

Results whose statement or proof uses this declaration.