François Clément
authored
Use unique_choice instead of choice when possible (Function_compl, AffineSpace, Finite_dim_R). Function_compl: Rename and move f_inv_EX -> bij_EX. Add and prove bij_ex. Extract inj_surj_ex_uniq{,_rev} from bij_ex_uniq{,_rev}. Simplify proofs of bij_equiv, bij_ex_uniq{,_rev}.
Name | Last commit | Last update |
---|