mathlib3

721bace8 - refactor(set_theory/ordinal_arithmetic): `omin` → `Inf` (#11867)

refactor(set_theory/ordinal_arithmetic): `omin` → `Inf` (#11867) We remove the redundant `omin` in favor of `Inf`. We also introduce a `conditionally_complete_linear_order_bot` instance on `cardinals`, and golf a particularly messy proof.