Mathlib Map

Theorems · Theorem · order theory

Left.inv_lt_one_iff

∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a : α}, a⁻¹ < 1 ↔ 1 < a

Uses left co(ntra)variant.

Defined in
Mathlib.Algebra.Order.Group.Unbundled.Basic
Cited by
5 results in Mathlib
Foundations
Depth 14 from the axioms · uses propext
Assumes
GroupLTMulLeftStrictMono
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

inv_lt_one' · cited by 2inv_lt_one'LinearOrderedCommGroup.Subgroup.exists_generator_lt_one · cited by 2Subgroup.exists_generator…inv_lt_one_iff_one_lt · cited by 1inv_lt_one_iff_one_ltone_lt_of_inv_lt_one · cited by 0one_lt_of_inv_lt_oneLeft.inv_lt_self · cited by 0Left.inv_lt_selfGroup · cited by 6238Groupmul_one · cited by 3885mul_oneMulLeftStrictMono · cited by 146MulLeftStrictMonomul_inv_cancel · cited by 128mul_inv_cancelmul_lt_mul_iff_left · cited by 14mul_lt_mul_iff_leftLeft.inv_lt_one_iffCITED BYCITES

Cites5

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

Cited by5

Results whose statement or proof uses this declaration.