Johan Commelin

icon indicating a website link — icon indicating an email [email protected]

icon company — icon location —

Results 183 comments of Johan Commelin

feat(set_theory/cardinal): cardinality of `multiset`, `polynomial` and `mv_polynomial`

bors d=vihdzp

feat(algebra/hom/centroid): Introduce the centroid of a (non-unital, non-associative) semiring

bors merge

feat(analysis/analytic/isolated_zeros): Principle of isolated zeros

Thanks :tada: bors merge

feat(analysis/analytic/isolated_zeros): Principle of isolated zeros

bors d+

feat(group_theory/divisible): definition of divisible group

Thanks :tada: bors merge

feat(group_theory/divisible): definition of divisible group

bors merge p=3

chore(*): restore `subsingleton` instances and remove hacks

Thanks :tada: bors merge

chore(*): restore `subsingleton` instances and remove hacks

bors merge p=3

feat(ring_theory/dedekind_domain/ideal): the prime factorizations of `r` and `span {r}` are essentially the same in a PID

bors merge p=4

feat(field_theory/splitting_field): Adjoining all of the roots of a polynomial gives a splitting field

bors merge p=4