Theorem Codisjoint.ne_bot_of_ne_top'

Modification history

2025-11-08 03:04

Mathlib/Order/Disjoint.lean

chore(Order): deprecate `Codisjoint.ne_bot_of_ne_top'`, `OrderEmbedding.{w,}covBy_of_apply` and `OrderIso.map_{w,}covBy` (#28486)

Modified Codisjoint.ne_bot_of_ne_top'View on Github →

2024-01-25 14:36

Mathlib/Order/Disjoint.lean

feat: define semisimple linear endomorphisms (#9825)

Added Codisjoint.ne_bot_of_ne_top'View on Github →