Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-11 08:13 e8839a30

View on Github →

refactor(logic/small, *): Infer f : α → β when followed by a simple condition on f (#11037)

Estimated changes

Modified src/data/equiv/encodable/small.lean

Modified src/data/equiv/set.lean

modified theorem equiv.apply_of_injective_symm

modified theorem equiv.coe_of_injective_symm

modified theorem equiv.of_injective_symm_apply

modified theorem equiv.self_comp_of_injective_symm

Modified src/data/fin/basic.lean

Modified src/group_theory/perm/sign.lean

Modified src/linear_algebra/basis.lean

Modified src/logic/small.lean

modified theorem small_of_injective

modified theorem small_of_surjective