Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Numeric non-zero equivalents/Redesign of Almost* properties in Algebra.Definitions #2117

Closed
wants to merge 12 commits into from
Closed

Numeric non-zero equivalents/Redesign of Almost* properties in Algebra.Definitions #2117

Changes from 1 commit
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
44163ba
`NonZero` constructor/destructor pairs for the concrete numeric types
jamesmckinna Sep 25, 2023
9c50a21
start on `AlmostCancellative` properties
jamesmckinna Sep 26, 2023
04a9c00
use of revised `Almost\*Commutative` definitions
jamesmckinna Sep 26, 2023
367dfa7
`CHANGELOG`
jamesmckinna Sep 26, 2023
849e706
`CHANGELOG`: removed changes to `Almost*Cancellative`
jamesmckinna Sep 26, 2023
5e8a45d
reconciled `Left\|RightConguent` with `Congruent₁
jamesmckinna Sep 26, 2023
ef3eb2b
Merge branch 'agda:master' into NumericNonZeroEquivalents
jamesmckinna Sep 29, 2023
b86aaef
preliminary redesign of `Almost*` algebraic properties
jamesmckinna Sep 30, 2023
7a6392c
two omitted arg reorderings
jamesmckinna Oct 1, 2023
f89a163
typo
jamesmckinna Oct 1, 2023
2373404
Update Definitions.agda: fixed typo
jamesmckinna Oct 1, 2023
2ec9bc3
Merge branch 'NumericNonZeroEquivalents' of github.com:jamesmckinna/a…
jamesmckinna Oct 1, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
CHANGELOG
  • Loading branch information
@jamesmckinna
jamesmckinna committed Sep 26, 2023
commit 367dfa7229d5a637807e893a844429e21af334eb
4 changes: 4 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1241,6 +1241,10 @@ Deprecated names
*-cancelˡ-<-neg ↦ *-cancelˡ-<-nonPos
*-cancelʳ-<-neg ↦ *-cancelʳ-<-nonPos

*-AlmostRightCancellative : AlmostRightCancellative 0ℤ _*_
*-AlmostLeftCancellative : AlmostLeftCancellative 0ℤ _*_
*-AlmostCancellative : AlmostCancellative 0ℤ _*_

^-semigroup-morphism ↦ ^-isMagmaHomomorphism
^-monoid-morphism ↦ ^-isMonoidHomomorphism

Expand Down