Theorem ExistsUnique.choose_eq_iff

Modification history

2026-01-03 16:31
Mathlib/Logic/ExistsUnique.lean
feat(ToIntervalMod): add missing lemmas (#33442) …
Added ExistsUnique.choose_eq_iffView on Github →