Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-04-13 19:25 7ebf83ed

View on Github →

chore(analysis/seminorm): add new le_def/lt_def and renaming (#18801)

Estimated changes

added theorem seminorm.coe_le_coe
added theorem seminorm.coe_lt_coe
modified theorem seminorm.le_def
modified theorem seminorm.lt_def