Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-09 09:36 13563978

View on Github →

refactor(linear_algebra/*): linear_equiv.of_bijective over semirings (#9061) linear_equiv.of_injective and linear_equiv.of_bijective took as assumption f.ker = \bot, which is equivalent to injectivity of f over rings, but not over semirings. This PR changes the assumption to injective f. For reasons of symmetry, the surjectivity assumption is also switched to surjective f. As a consequence, this PR also renames:

linear_equiv_of_ker_eq_bot to linear_equiv_of_injective
linear_equiv_of_ker_eq_bot_apply to linear_equiv_of_injective_apply

Estimated changes

Modified src/algebra/category/Module/subobject.lean

Modified src/algebra/lie/subalgebra.lean

Modified src/analysis/normed_space/banach.lean

Modified src/analysis/normed_space/bounded_linear_maps.lean

Modified src/analysis/normed_space/finite_dimension.lean

Modified src/analysis/normed_space/linear_isometry.lean

Modified src/linear_algebra/basic.lean

modified def linear_equiv.arrow_congr

modified theorem linear_equiv.arrow_congr_apply

modified theorem linear_equiv.arrow_congr_symm_apply

modified theorem linear_equiv.of_injective_apply

Modified src/linear_algebra/bilinear_form.lean

added theorem bilin_form.nondegenerate.ker_eq_bot

Modified src/linear_algebra/dimension.lean

Modified src/linear_algebra/dual.lean

Modified src/linear_algebra/finite_dimensional.lean

modified theorem linear_equiv.coe_of_injective_endo

modified theorem linear_equiv.of_injective_endo_left_inv

modified theorem linear_equiv.of_injective_endo_right_inv

added theorem linear_map.linear_equiv_of_injective_apply

deleted theorem linear_map.linear_equiv_of_ker_eq_bot_apply

Modified src/linear_algebra/free_module_pid.lean

Modified src/linear_algebra/linear_independent.lean

Modified src/linear_algebra/matrix/to_linear_equiv.lean

Modified src/linear_algebra/projection.lean

Modified src/ring_theory/noetherian.lean