Diffusion Isabelle d56e4eeae967

mult_le_cancel_iff1, mult_le_cancel_iff2, mult_less_iff1 generalised from the…
d56e4eeae967
Actions

Tags

None

Subscribers

None

Description

mult_le_cancel_iff1, mult_le_cancel_iff2, mult_less_iff1 generalised from the real_ versions

Details

Provenance

paulson <lp15@cam.ac.uk>

Authored on

Parents

rISABELLEbac8921e2901: merged

Branches

Unknown

Tags

Unknown

Event Timeline

paulson <lp15@cam.ac.uk> committed rISABELLEd56e4eeae967: mult_le_cancel_iff1, mult_le_cancel_iff2, mult_less_iff1 generalised from the….Nov 11 2020, 3:27 PM

Changes (15)

Path

Size

src/

HOL/

Analysis/

Brouwer_Fixpoint.thy

Change_Of_Vars.thy

Elementary_Metric_Spaces.thy

Equivalence_Lebesgue_Henstock_Integration.thy

Henstock_Kurzweil_Integration.thy

Homeomorphism.thy

Line_Segment.thy

Tagged_Division.thy

Vitali_Covering_Theorem.thy

rISABELLEd56e4eeae967

src/HOL/Analysis/Brouwer_Fixpoint.thy

Loading...

src/HOL/Analysis/Change_Of_Vars.thy

Loading...

src/HOL/Analysis/Derivative.thy

Loading...

src/HOL/Analysis/Elementary_Metric_Spaces.thy

Loading...

src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy

Loading...

src/HOL/Analysis/Henstock_Kurzweil_Integration.thy

Loading...

src/HOL/Analysis/Homeomorphism.thy

Loading...

src/HOL/Analysis/Line_Segment.thy

Loading...

src/HOL/Analysis/Poly_Roots.thy

Loading...

src/HOL/Analysis/Polytope.thy

Loading...

src/HOL/Analysis/Starlike.thy

Loading...

src/HOL/Analysis/Tagged_Division.thy

Loading...

src/HOL/Analysis/Vitali_Covering_Theorem.thy

Loading...

src/HOL/Factorial.thy

Loading...

src/HOL/Real.thy

Loading...