Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-19 09:07 77f5fb33

View on Github →

feat(linear_algebra/eigenspace): mem_maximal_generalized_eigenspace (#7162)

Estimated changes

Modified src/linear_algebra/basic.lean

added theorem submodule.coe_scott_continuous

added theorem submodule.coe_supr_of_chain

added theorem submodule.mem_supr_of_chain

Modified src/linear_algebra/eigenspace.lean

added theorem module.End.generalized_eigenspace_le_maximal

added theorem module.End.mem_generalized_eigenspace

added theorem module.End.mem_maximal_generalized_eigenspace

Modified src/order/directed.lean

added theorem monotone.directed_le