Commit 2025-03-21 14:18 8bb33f4e

View on Github →

chore: generalise ENat.iInf_eq_zero (#23180) Previously, it had f : ι → ℕ. Also make it simp.

Estimated changes