Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-30 07:34 e1fa5cba

View on Github →

feat(linear_algebra): invariant basis number property (#3560)

Estimated changes

Modified src/linear_algebra/basic.lean

added theorem submodule.bot_ne_top

Created src/linear_algebra/invariant_basis_number.lean

added theorem eq_of_fin_equiv

added theorem invariant_basis_number_field

added theorem nontrivial_of_invariant_basis_number

Modified src/ring_theory/ideals.lean

added theorem ideal.map_pi

added theorem ideal.mem_pi

added def ideal.pi