Theorem EReal.induction₂_symm

Modification history

2024-03-01 13:29

Mathlib/Data/Real/EReal.lean

refactor: induction₂_symm: Be more explicit in the case variables (#11023) …

Modified EReal.induction₂_symm View on Github →

2023-02-28 07:22

Mathlib/Data/Real/EReal.lean

feat: port Data.Real.EReal (#2501)

Added EReal.induction₂_symm View on Github →