PR #15644: feat(algebra/order/with_zero): Add eq_one_of_m...

Stream: triage

[Random Issue Bot]

Today I chose PR 15644 for discussion!

feat(algebra/order/with_zero): Add eq_one_of_mul_eq_one lemmas
Created by @David Kurniadi Angdinata (@Multramate) on 2022-07-23
Labels: awaiting-review

Is this PR still relevant? Any recent updates? Anyone making progress?