mechvel

I am sorry. If the Binary.DivMod PR has not disappeared, then, please, consider this DivMod. If you also can add there Algebra.Properties.Semigroup, then all right. If not, then let us...

>> I suggest to generalize this to IsNonzero : Pred Carrier _ >> and Nonzero = Σ Carrier IsNonzero, >> We should not generalise the existing examples in Nat, Integer...

Currently I use this general definition under `Semiring` : ``` NonZero = Σ Carrier (_≉ 0#) ``` And now I propose instead (for Standard): ``` data ButOne (b : Carrier)...

Of course, a definition for `NonZero` must not rely on a decidable equality. Also it is regularly is needed ``NonZero? : Decidable NonZero`` -- and it is for the domains...

Jacques writes. > That way the decidable domains can be maximally usable. The other domains should be hard to deal with (constructively)! There is some mystery secret about this. 1)...

> And they also define field structure here > [..] It is desirable for Standard to intoduce the Field abstract domain: (Def) A CommutativeRing is a Field, when it has...

Jacques writes > Even classically, Field is weird: it's not given equationally. Fields do not form a variety. I recall, after my talk in 2013 Jacques asked me: why do...

May be it is all right for Standard to have a Setoid-based Algebra only. But it is natural for applied libraries to have dec-versions. For example, on practice one very...

I do not think that Matrix is for standard library. Rather it needs to be for the application libraries. If matrices, then there will go module bases and homomorphisms by...

> I still feel that this part of the library feels the worst organised as at the moment > Algebra.Operations.CommutativeMonoid contains many properties as well, not just simply > operations....