Instances and theorems on pi types #
This file provides instances for the typeclass defined in Algebra.Group.Defs
. More sophisticated
instances are defined in Algebra.Group.Pi.Lemmas
files elsewhere.
Porting note #
This file relied on the pi_instance
tactic, which was not available at the time of porting. The
comment --pi_instance
is inserted before all fields which were previously derived by
pi_instance
. See this Zulip discussion:
[https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/not.20porting.20pi_instance]
1
, 0
, +
, *
, +ᵥ
, •
, ^
, -
, ⁻¹
, and /
are defined pointwise.
Equations
- Pi.addSemigroup = AddSemigroup.mk ⋯
Equations
- Pi.semigroup = Semigroup.mk ⋯
Equations
- Pi.addCommSemigroup = AddCommSemigroup.mk ⋯
Equations
- Pi.commSemigroup = CommSemigroup.mk ⋯
Equations
- Pi.addZeroClass = AddZeroClass.mk ⋯ ⋯
Equations
- Pi.mulOneClass = MulOneClass.mk ⋯ ⋯
Equations
- Pi.negZeroClass = NegZeroClass.mk ⋯
Equations
- Pi.invOneClass = InvOneClass.mk ⋯
Equations
- Pi.addMonoid = AddMonoid.mk ⋯ ⋯ (fun (n : ℕ) (x : (i : I) → f i) (i : I) => n • x i) ⋯ ⋯
Equations
- Pi.addCommMonoid = AddCommMonoid.mk ⋯
Equations
- Pi.commMonoid = CommMonoid.mk ⋯
Equations
- Pi.subNegMonoid = SubNegMonoid.mk ⋯ (fun (z : ℤ) (x : (i : I) → f i) (i : I) => z • x i) ⋯ ⋯ ⋯
Equations
- Pi.divInvMonoid = DivInvMonoid.mk ⋯ (fun (z : ℤ) (x : (i : I) → f i) (i : I) => x i ^ z) ⋯ ⋯ ⋯
Equations
- Pi.subNegZeroMonoid = SubNegZeroMonoid.mk ⋯
Equations
- Pi.divInvOneMonoid = DivInvOneMonoid.mk ⋯
Equations
- Pi.involutiveNeg = InvolutiveNeg.mk ⋯
Equations
- Pi.involutiveInv = InvolutiveInv.mk ⋯
Equations
- Pi.subtractionMonoid = SubtractionMonoid.mk ⋯ ⋯ ⋯
Equations
- Pi.divisionMonoid = DivisionMonoid.mk ⋯ ⋯ ⋯
Equations
- Pi.instSubtractionCommMonoid = SubtractionCommMonoid.mk ⋯
Equations
- Pi.divisionCommMonoid = DivisionCommMonoid.mk ⋯
Equations
- Pi.addGroup = AddGroup.mk ⋯
Equations
- Pi.addCommGroup = AddCommGroup.mk ⋯
Equations
- Pi.commGroup = CommGroup.mk ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- Pi.addLeftCancelSemigroup = AddLeftCancelSemigroup.mk ⋯
Equations
- Pi.leftCancelSemigroup = LeftCancelSemigroup.mk ⋯
Equations
- Pi.addRightCancelSemigroup = AddRightCancelSemigroup.mk ⋯
Equations
- Pi.rightCancelSemigroup = RightCancelSemigroup.mk ⋯
Equations
- Pi.addLeftCancelMonoid = AddLeftCancelMonoid.mk ⋯
Equations
- Pi.leftCancelMonoid = LeftCancelMonoid.mk ⋯
Equations
- Pi.addRightCancelMonoid = AddRightCancelMonoid.mk ⋯
Equations
- Pi.rightCancelMonoid = RightCancelMonoid.mk ⋯
Equations
- Pi.addCancelMonoid = AddCancelMonoid.mk ⋯
Equations
- Pi.cancelMonoid = CancelMonoid.mk ⋯
Equations
- Pi.addCancelCommMonoid = AddCancelCommMonoid.mk ⋯
Equations
- Pi.cancelCommMonoid = CancelCommMonoid.mk ⋯
The function supported at i
, with value x
there, and 0
elsewhere.
Equations
- Pi.single i x = Function.update 0 i x
The function supported at i
, with value x
there, and 1
elsewhere.
Equations
- Pi.mulSingle i x = Function.update 1 i x
Abbreviation for single_eq_of_ne h.symm
, for ease of use by simp
.
Abbreviation for mulSingle_eq_of_ne h.symm
, for ease of use by simp
.
On non-dependent functions, Pi.mulSingle
can be expressed as an ite
On non-dependent functions, Pi.single
is symmetric in the two indices.
On non-dependent functions, Pi.mulSingle
is symmetric in the two indices.
If the zero function is surjective, the codomain is trivial.
Equations
If the one function is surjective, the codomain is trivial.