HomeIsabelle/Phabricator

Renamed the misleading has_field_derivative_iff_has_vector_derivative. Inserted…

Description

Renamed the misleading has_field_derivative_iff_has_vector_derivative. Inserted a number of minor lemmas

Details

Provenance
paulson <lp15@cam.ac.uk>Authored on
Parents
rISABELLE4c3bc0d2568f: Eliminated two unnecessary inductions
Branches
Unknown
Tags
Unknown