Commit 2023-07-06 06:47 f4e42872

View on Github →

chore: rename Fin.castSucc to Fin.castSuccEmb (#5729)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Fin.lean

deleted theorem Fin.prod_univ_castSucc

added theorem Fin.prod_univ_castSuccEmb

Modified Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean

Modified Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean

Modified Mathlib/AlgebraicTopology/DoldKan/Faces.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory.lean

modified theorem SimplexCategory.δ_comp_δ''

modified theorem SimplexCategory.δ_comp_δ'

modified theorem SimplexCategory.δ_comp_δ_self'

modified theorem SimplexCategory.δ_comp_δ_self

modified theorem SimplexCategory.δ_comp_σ_of_gt

modified theorem SimplexCategory.δ_comp_σ_of_le

modified theorem SimplexCategory.δ_comp_σ_self'

Modified Mathlib/AlgebraicTopology/SimplicialObject.lean

modified theorem CategoryTheory.CosimplicialObject.δ_comp_δ''

modified theorem CategoryTheory.CosimplicialObject.δ_comp_δ'

modified theorem CategoryTheory.CosimplicialObject.δ_comp_δ_self'

modified theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt

modified theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_le

modified theorem CategoryTheory.CosimplicialObject.δ_comp_σ_self'

modified theorem CategoryTheory.CosimplicialObject.δ_comp_σ_self

modified theorem CategoryTheory.SimplicialObject.δ_comp_δ''

modified theorem CategoryTheory.SimplicialObject.δ_comp_δ'

modified theorem CategoryTheory.SimplicialObject.δ_comp_δ_self'

modified theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_gt

modified theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_le

modified theorem CategoryTheory.SimplicialObject.δ_comp_σ_self'

modified theorem CategoryTheory.SimplicialObject.δ_comp_σ_self

Modified Mathlib/Analysis/NormedSpace/Multilinear.lean

Modified Mathlib/Analysis/SchwartzSpace.lean

Modified Mathlib/Data/Fin/Basic.lean

deleted theorem Fin.castIso_castSucc

added theorem Fin.castIso_castSuccEmb

deleted theorem Fin.castLT_castSucc

added theorem Fin.castLT_castSuccEmb

modified theorem Fin.castLT_succAbove

deleted theorem Fin.castPred_castSucc

added theorem Fin.castPred_castSuccEmb

deleted def Fin.castSucc

added def Fin.castSuccEmb

added theorem Fin.castSuccEmb_castLT

added theorem Fin.castSuccEmb_castPred

added theorem Fin.castSuccEmb_eq_zero_iff

added theorem Fin.castSuccEmb_fin_succ

added theorem Fin.castSuccEmb_inj

added theorem Fin.castSuccEmb_injective

added theorem Fin.castSuccEmb_lt_castSuccEmb_iff

added theorem Fin.castSuccEmb_lt_iff_succ_le

added theorem Fin.castSuccEmb_lt_last

added theorem Fin.castSuccEmb_lt_succ

added theorem Fin.castSuccEmb_mk

added theorem Fin.castSuccEmb_ne_zero_iff

added theorem Fin.castSuccEmb_one

added theorem Fin.castSuccEmb_pos

added theorem Fin.castSuccEmb_pred_eq_pred_castSuccEmb

added theorem Fin.castSuccEmb_zero

deleted theorem Fin.castSucc_castLT

deleted theorem Fin.castSucc_castPred

deleted theorem Fin.castSucc_eq_zero_iff

deleted theorem Fin.castSucc_fin_succ

deleted theorem Fin.castSucc_inj

deleted theorem Fin.castSucc_injective

deleted theorem Fin.castSucc_lt_castSucc_iff

deleted theorem Fin.castSucc_lt_iff_succ_le

deleted theorem Fin.castSucc_lt_last

deleted theorem Fin.castSucc_lt_succ

deleted theorem Fin.castSucc_mk

deleted theorem Fin.castSucc_ne_zero_iff

deleted theorem Fin.castSucc_one

deleted theorem Fin.castSucc_pos

deleted theorem Fin.castSucc_pred_eq_pred_castSucc

deleted theorem Fin.castSucc_zero

modified theorem Fin.coeSucc_eq_succ

deleted theorem Fin.coe_castSucc

added theorem Fin.coe_castSuccEmb

deleted theorem Fin.coe_eq_castSucc

added theorem Fin.coe_eq_castSuccEmb

added theorem Fin.coe_of_injective_castSuccEmb_symm

deleted theorem Fin.coe_of_injective_castSucc_symm

added theorem Fin.exists_castSuccEmb_eq

deleted theorem Fin.exists_castSucc_eq

deleted theorem Fin.lastCases_castSucc

added theorem Fin.lastCases_castSuccEmb

added theorem Fin.le_castSuccEmb_iff

deleted theorem Fin.le_castSucc_iff

modified theorem Fin.lt_succ

modified theorem Fin.lt_succAbove_iff

deleted theorem Fin.natAdd_castSucc

added theorem Fin.natAdd_castSuccEmb

modified theorem Fin.predAbove_above

modified theorem Fin.predAbove_below

added theorem Fin.pred_castSuccEmb_succ

deleted theorem Fin.pred_castSucc_succ

modified theorem Fin.pred_succAbove

deleted theorem Fin.range_castSucc

added theorem Fin.range_castSuccEmb

deleted theorem Fin.reverse_induction_castSucc

added theorem Fin.reverse_induction_castSuccEmb

modified theorem Fin.succAbove_above

modified theorem Fin.succAbove_below

modified theorem Fin.succAbove_last

modified theorem Fin.succAbove_last_apply

modified theorem Fin.succAbove_lt_ge

modified theorem Fin.succAbove_lt_gt

modified theorem Fin.succAbove_lt_iff

modified theorem Fin.succAbove_predAbove

deleted theorem Fin.succ_castSucc

added theorem Fin.succ_castSuccEmb

Modified Mathlib/Data/Fin/Tuple/Basic.lean

modified def Fin.init

deleted theorem Fin.init_update_castSucc

added theorem Fin.init_update_castSuccEmb

modified def Fin.snoc

deleted theorem Fin.snoc_castSucc

added theorem Fin.snoc_castSuccEmb

modified theorem Fin.snoc_cast_add

deleted theorem Fin.snoc_comp_castSucc

added theorem Fin.snoc_comp_castSuccEmb

modified theorem Fin.snoc_update

Modified Mathlib/Data/Fin/Tuple/Monotone.lean

Modified Mathlib/Data/Fin/Tuple/Reflection.lean

Modified Mathlib/Data/Fintype/Basic.lean

deleted theorem Fin.image_castSucc

added theorem Fin.image_castSuccEmb

deleted theorem Fin.univ_castSucc

added theorem Fin.univ_castSuccEmb

Modified Mathlib/Data/Fintype/Fin.lean

deleted theorem Fin.Iio_castSucc

added theorem Fin.Iio_castSuccEmb

modified theorem Fin.Iio_last_eq_map

Modified Mathlib/Data/List/OfFn.lean

Modified Mathlib/Data/Polynomial/EraseLead.lean

Modified Mathlib/Data/Sym/Card.lean

Modified Mathlib/Data/Vector/Basic.lean

Modified Mathlib/GroupTheory/Perm/Fin.lean

Modified Mathlib/LinearAlgebra/FreeModule/StrongRankCondition.lean

Modified Mathlib/LinearAlgebra/Matrix/Determinant.lean

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

modified theorem MultilinearMap.snoc_add

modified theorem MultilinearMap.snoc_smul

Modified Mathlib/LinearAlgebra/Vandermonde.lean

Modified Mathlib/Logic/Equiv/Fin.lean

modified theorem finSuccEquiv'_above

modified theorem finSuccEquiv'_below

deleted theorem finSuccEquiv'_last_apply_castSucc

added theorem finSuccEquiv'_last_apply_castSuccEmb

modified theorem finSuccEquiv'_symm_coe_above

modified theorem finSuccEquiv'_symm_coe_below

modified theorem finSuccEquiv'_symm_some_above

modified theorem finSuccEquiv'_symm_some_below

deleted theorem finSuccEquivLast_castSucc

added theorem finSuccEquivLast_castSuccEmb

modified theorem finSuccEquivLast_symm_some

Modified Mathlib/ModelTheory/Semantics.lean

Modified Mathlib/ModelTheory/Ultraproducts.lean

Modified Mathlib/Order/JordanHolder.lean

deleted theorem CompositionSeries.snoc_castSucc

added theorem CompositionSeries.snoc_castSuccEmb

Modified Mathlib/RepresentationTheory/GroupCohomology/Basic.lean

Modified Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

Modified Mathlib/RingTheory/ChainOfDivisors.lean