Paul Lezeau

icon location PhD student @ LSGNT (Imperial College, King's College London and University College London)

Results 1 comments of Paul Lezeau

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

Lean seems to have trouble finding the instance `decidable_rel (( | ) : ideal R \to ideal R \to Prop)` in the proof of `multiplicity_eq_multiplicity_span`. Any fix would be more...