/
pi.lean
72 lines (54 loc) · 2.12 KB
/
pi.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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
/-
Copyright (c) 2020 Eric Wieser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon, Patrick Massot, Eric Wieser
-/
import tactic.split_ifs
import tactic.simpa
import algebra.group.to_additive
/-!
# Instances and theorems on pi types
This file provides basic definitions and notation instances for Pi types.
Instances of more sophisticated classes are defined in `pi.lean` files elsewhere.
-/
universes u v w
variable {I : Type u} -- The indexing type
variable {f : I → Type v} -- The family of types already equipped with instances
variables (x y : Π i, f i) (i : I)
namespace pi
/-! `1`, `0`, `+`, `*`, `-`, `⁻¹`, and `/` are defined pointwise. -/
@[to_additive] instance has_one [∀ i, has_one $ f i] :
has_one (Π i : I, f i) :=
⟨λ _, 1⟩
@[simp, to_additive] lemma one_apply [∀ i, has_one $ f i] : (1 : Π i, f i) i = 1 := rfl
@[to_additive] lemma one_def [Π i, has_one $ f i] : (1 : Π i, f i) = λ i, 1 := rfl
@[to_additive]
instance has_mul [∀ i, has_mul $ f i] :
has_mul (Π i : I, f i) :=
⟨λ f g i, f i * g i⟩
@[simp, to_additive] lemma mul_apply [∀ i, has_mul $ f i] : (x * y) i = x i * y i := rfl
@[to_additive] instance has_inv [∀ i, has_inv $ f i] :
has_inv (Π i : I, f i) :=
⟨λ f i, (f i)⁻¹⟩
@[simp, to_additive] lemma inv_apply [∀ i, has_inv $ f i] : x⁻¹ i = (x i)⁻¹ := rfl
@[to_additive] instance has_div [Π i, has_div $ f i] :
has_div (Π i : I, f i) :=
⟨λ f g i, f i / g i⟩
@[simp, to_additive] lemma div_apply [Π i, has_div $ f i] : (x / y) i = x i / y i := rfl
section
variables [decidable_eq I]
variables [Π i, has_zero (f i)]
/-- The function supported at `i`, with value `x` there. -/
def single (i : I) (x : f i) : Π i, f i :=
function.update 0 i x
@[simp]
lemma single_eq_same (i : I) (x : f i) : single i x i = x :=
function.update_same i x _
@[simp]
lemma single_eq_of_ne {i i' : I} (h : i' ≠ i) (x : f i) : single i x i' = 0 :=
function.update_noteq h x _
variables (f)
lemma single_injective (i : I) : function.injective (single i : f i → Π i, f i) :=
function.update_injective _ i
end
end pi