Theorem equiv.of_injective_symm_apply
Modification history
2022-01-11 08:13
src/data/equiv/set.lean
refactor(logic/small, *): Infer `f : α → β` when followed by a simple condition on `f` (#11037)
Modified equiv.of_injective_symm_applyView on Github →