Functional vector module - #1945

Closed

guilhermehas wants to merge 25 commits into

agda:masterfrom

guilhermehas:functional-vector-module

Commits on Apr 17, 2023

added Functional Algebra Properties
guilhermehas
committed
a295308
put some things in Base
guilhermehas
committed
3037439
added changelog
guilhermehas
committed
468bb69
added the names
guilhermehas
committed
700b114
changed VC to Vector Carrier
guilhermehas
committed
623d474
changed semiGroup to semigroup
guilhermehas
committed
a5f6a10
modified the CHANGELOG
guilhermehas
committed
514ef92
added all the definitions
guilhermehas
committed
ce75303
changed to commutative ring to add module
guilhermehas
committed
7d62c1c
fixed isModule
guilhermehas
committed
3ed6e0b

Commits on Apr 18, 2023

added ring * and 1m
guilhermehas
committed
81548b0
add all operators of functional vec
guilhermehas
committed
1b684fc

Commits on May 18, 2023

changed the code to be more general
guilhermehas
committed
6604b6e

Commits on May 19, 2023

using rawStructures instead
guilhermehas
committed
bc7d02d

Commits on May 25, 2023

fixed base exportation
guilhermehas
committed
51a8adc

Commits on May 26, 2023

proved more definitions
guilhermehas
committed
841be8c
added monoid properties
guilhermehas
committed
62b0af2
added isGroup and isAbGroup
guilhermehas
committed
651c316
added semiring properties
guilhermehas
committed
1c520d1
added Ring Properties
guilhermehas
committed
2f9e635
changed back to espilon and dot definition
guilhermehas
committed
9fc2632
added magma definitions
guilhermehas
committed
e39e20e
added some more groups
guilhermehas
committed
59e693e

Commits on May 27, 2023

added structures inside
guilhermehas
committed
967be03
added the bundles
guilhermehas
committed
4dccb0e