Theorems · Theorem · order theory

IsOrderedAddMonoid.mkOfCone

∀ {S : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : SetLike S G] (C : S) [inst_2 : AddGroupConeClass S G],
  have x := PartialOrder.mkOfAddGroupCone C;
  IsOrderedAddMonoid G

Construct a partially ordered abelian group by designating a cone in an abelian group.

Defined in: Mathlib.Algebra.Order.Group.Cone
Cited by: 0 results in Mathlib
Foundations: Depth 16 from the axioms · uses propext
Assumes: AddCommGroup SetLike AddGroupConeClass

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites7

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

AddCommGroupstatement and proof · cited by 12,871
PartialOrderstatement and proof · cited by 6,410
IsOrderedAddMonoidstatement · cited by 1,659
SetLikestatement and proof · cited by 1,084
add_sub_add_right_eq_subproof · cited by 29
AddGroupConeClassstatement and proof · cited by 3
PartialOrder.mkOfAddGroupConestatement and proof · cited by 3

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.