Commit 2023-04-12 19:26 10dd3d5e

View on Github →

chore: rename castLe (#3326)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Fin.lean

Modified Mathlib/Combinatorics/Composition.lean

Modified Mathlib/Data/Fin/Basic.lean

added def Fin.castLE

added theorem Fin.castLE_castLE

added theorem Fin.castLE_comp_castLE

added theorem Fin.castLE_mk

added theorem Fin.castLE_of_eq

added theorem Fin.castLE_succ

added theorem Fin.castLE_zero

deleted def Fin.castLe

deleted theorem Fin.castLe_castLe

deleted theorem Fin.castLe_comp_castLe

deleted theorem Fin.castLe_mk

deleted theorem Fin.castLe_of_eq

deleted theorem Fin.castLe_succ

deleted theorem Fin.castLe_zero

added theorem Fin.coe_castLE

deleted theorem Fin.coe_castLe

added theorem Fin.coe_of_injective_castLE_symm

deleted theorem Fin.coe_of_injective_castLe_symm

added theorem Fin.range_castLE

deleted theorem Fin.range_castLe

Modified Mathlib/Data/Finset/Sort.lean

Modified Mathlib/Data/Fintype/Card.lean

Modified Mathlib/GroupTheory/Perm/Fin.lean

Modified Mathlib/LinearAlgebra/InvariantBasisNumber.lean

Modified Mathlib/Logic/Equiv/Fin.lean

added def Fin.castLEOrderIso

deleted def Fin.castLeOrderIso