Theorem Fin.bot_eq_zero

Modification history

2026-05-23 11:09
Mathlib/Order/Fin/Basic.lean
chore: `IsBotZeroClass (Fin n)` (#39058) …
Deleted Fin.bot_eq_zeroView on Github →
2025-01-28 16:01
Mathlib/Order/Fin/Basic.lean
feat(*/Fin/*): add lemmas (#21175) …
Modified Fin.bot_eq_zeroView on Github →
2024-05-23 11:18
Mathlib/Data/Fin/Basic.lean
chore: Remove order dependencies to `Data.Fin.Basic` (#13005) …
Modified Fin.bot_eq_zeroView on Github →
2023-01-12 19:47
Mathlib/Data/Fin/Basic.lean
feat: port Data.Fin.Basic (#1084) …
Added Fin.bot_eq_zeroView on Github →