No results found

flt-regular

Proof of Kaplanski criterion for being a UFD in Lean4