Commit 2023-01-06 22:29 47a1fd99
View on Github →feat: remove final sorries in positivity tactic (#1375) Per https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Last.20sorries.20in.20mathlib4
feat: remove final sorries in positivity tactic (#1375) Per https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Last.20sorries.20in.20mathlib4