-
Notifications
You must be signed in to change notification settings - Fork 257
/
Defs.lean
41 lines (32 loc) · 1.18 KB
/
Defs.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
/-
Copyright (c) 2014 Parikshit Khanna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
-/
import Mathlib.Algebra.Group.Defs
#align_import data.list.defs from "leanprover-community/mathlib"@"d2d8742b0c21426362a9dacebc6005db895ca963"
/-!
## Products and sums over lists
-/
namespace List
/-- Product of a list.
`List.prod [a, b, c] = ((1 * a) * b) * c` -/
@[to_additive "Sum of a list.\n\n`List.sum [a, b, c] = ((0 + a) + b) + c`"]
def prod {α} [Mul α] [One α] : List α → α :=
foldl (· * ·) 1
#align list.prod List.prod
#align list.sum List.sum
/-- The alternating sum of a list. -/
def alternatingSum {G : Type*} [Zero G] [Add G] [Neg G] : List G → G
| [] => 0
| g :: [] => g
| g :: h :: t => g + -h + alternatingSum t
#align list.alternating_sum List.alternatingSum
/-- The alternating product of a list. -/
@[to_additive existing]
def alternatingProd {G : Type*} [One G] [Mul G] [Inv G] : List G → G
| [] => 1
| g :: [] => g
| g :: h :: t => g * h⁻¹ * alternatingProd t
#align list.alternating_prod List.alternatingProd
end List