Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-04-06 12:45 67e606ea

View on Github →

chore(linear_algebra/dimension): fix lemma names (#18747) This fixes some lemma names which use rank but are about finrank:

rank_sup_add_rank_inf_eq → submodule.rank_sup_add_rank_inf_eq
rank_add_le_rank_add_rank → submodule.rank_add_le_rank_add_rank
submodule.rank_sup_add_rank_inf_eq → submodule.finrank_sup_add_finrank_inf_eq
submodule.rank_add_le_rank_add_rank → submodule.finrank_add_le_finrank_add_finrank

Estimated changes

Modified archive/sensitivity.lean

Modified src/analysis/inner_product_space/projection.lean

Modified src/linear_algebra/affine_space/finite_dimensional.lean

Modified src/linear_algebra/bilinear_form.lean

Modified src/linear_algebra/dimension.lean

deleted theorem rank_add_le_rank_add_rank

deleted theorem rank_sup_add_rank_inf_eq

added theorem submodule.rank_add_le_rank_add_rank

added theorem submodule.rank_sup_add_rank_inf_eq

Modified src/linear_algebra/finite_dimensional.lean

added theorem submodule.finrank_add_le_finrank_add_finrank

added theorem submodule.finrank_sup_add_finrank_inf_eq

deleted theorem submodule.rank_add_le_rank_add_rank

deleted theorem submodule.rank_sup_add_rank_inf_eq