Mathlib v3 is deprecated. Go to Mathlib v4

Def is_well_order.to_has_well_founded

Modification history

2022-06-10 10:43
src/order/rel_classes.lean
feat(analysis/inner_product_space): Generalize Gram-Schmidt (#14379) …
Added is_well_order.to_has_well_foundedView on Github →