Mathlib Map

Theorems · Theorem · order theory

mabs_mabs

∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α] [MulRightMono α] (a : α), |(|a|ₘ)|ₘ = |a|ₘ
Defined in
Mathlib.Algebra.Order.Group.Unbundled.Abs
Cited by
2 results in Mathlib
Foundations
Depth 30 from the axioms · uses propext, Quot.sound
Assumes
LatticeGroupMulLeftMonoMulRightMono
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

MulArchimedeanClass.mk_mabs · cited by 2MulArchimedeanClass.mk_ma…comap_mabs_nhds_one · cited by 1comap_mabs_nhds_oneGroup · cited by 6238GroupLattice · cited by 916LatticeMulLeftMono · cited by 410MulLeftMonoMulRightMono · cited by 263MulRightMonomabs · cited by 148mabsmabs_of_one_le · cited by 11mabs_of_one_leone_le_mabs · cited by 11one_le_mabsmabs_mabsCITED BYCITES

Cites7

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

Cited by2

Results whose statement or proof uses this declaration.