Commit 2023-04-07 17:47 a78e52ba

View on Github →

feat: port Analysis.Hofer (#3321)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Hofer.lean

added theorem hofer

added theorem pos_div_pow_pos