-
Notifications
You must be signed in to change notification settings - Fork 1
/
abelian group.slate
36 lines (34 loc) · 1.02 KB
/
abelian group.slate
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
%../../../../logics/hlm%
[
$~Operations = $../../Essentials/Operations
]
/**
* @references * https://en.wikipedia.org/wiki/Abelian_group
* * https://mathworld.wolfram.com/Abelian.html
* * https://proofwiki.org/wiki/Definition:Abelian_Group
* * https://ncatlab.org/nlab/show/abelian+group
* * https://leanprover-community.github.io/mathlib_docs/algebra/group/basic.html#comm_group
*/
$"abelian group"(
G: %Set,
∗: %Element($~Operations/"Inner operations"(X = G)),
e: %Element(G),
i: %Element($../../Essentials/Functions/Functions(X = G, Y = G))
): %Predicate {
notation = $Structure(
items = [G, ∗, e, i],
singular = 'abelian group',
plural = 'abelian groups',
article = 'an'
),
definition = [
%and(
$group(G = G, ∗ = ∗, e = e, i = i),
$abelian(𝐆 = $Groups.group(G = G, ∗ = ∗, e = e, i = i))
),
%and(
$group(G = G, ∗ = ∗, e = e, i = i),
$~Operations/commutative(X = G, Z = G, ∗ = ∗)
)
]
}