Notation for algebraic operators on pi types #
This file provides only the notation for (pointwise) 0
, 1
, +
, *
, •
, ^
, ⁻¹
on pi types.
See Mathlib/Algebra/Group/Pi/Basic.lean
for the Monoid
and Group
instances.
1
, 0
, +
, *
, +ᵥ
, •
, ^
, -
, ⁻¹
, and /
are defined pointwise.
Equations
- Pi.instOne = { one := fun (x : ι) => 1 }
Equations
- Pi.instZero = { zero := fun (x : ι) => 0 }
@[simp]
@[simp]