ULift
instances for groups and monoids #
This file defines instances for group, monoid, semigroup and related structures on ULift
types.
(Recall ULift α
is just a "copy" of a type α
in a higher universe.)
We also provide MulEquiv.ulift : ULift R ≃* R
(and its additive analogue).
Equations
- ULift.zero = { zero := { down := 0 } }
Equations
- ULift.smul = { smul := fun (n : α) (x : ULift.{?u.4, ?u.5} β) => { down := n • x.down } }
Equations
- ULift.vadd = { vadd := fun (n : α) (x : ULift.{?u.4, ?u.5} β) => { down := n +ᵥ x.down } }
The multiplicative equivalence between ULift α
and α
.
Equations
- MulEquiv.ulift = { toEquiv := Equiv.ulift, map_mul' := ⋯ }
Instances For
The additive equivalence between ULift α
and α
.
Equations
- AddEquiv.ulift = { toEquiv := Equiv.ulift, map_add' := ⋯ }
Instances For
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
- ULift.instNatCast = { natCast := fun (x : ℕ) => { down := ↑x } }
Equations
- ULift.instIntCast = { intCast := fun (x : ℤ) => { down := ↑x } }
@[simp]
@[simp]
Equations
Equations
Equations
- ULift.divInvMonoid = Function.Injective.divInvMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- ULift.subNegAddMonoid = Function.Injective.subNegMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- ULift.group = Function.Injective.group ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- ULift.addGroup = Function.Injective.addGroup ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- ULift.commGroup = Function.Injective.commGroup ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- ULift.addCommGroup = Function.Injective.addCommGroup ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- ULift.addGroupWithOne = AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯