Def {u}
Modification history
2023-01-31 16:05
src/data/quot.lean
feat(data/quot): make `trunc` a `quotient` (#18320) …
Modified {u}View on Github →2022-11-23 00:20
src/probability/probability_mass_function/basic.lean
feat(probability/probability_mass_function/*): Define `pmf` in terms of `ennreal` instead of `nnreal` (#17032) …
Modified {u}View on Github →2021-11-13 10:27
src/measure_theory/probability_mass_function/basic.lean
chore(measure_theory/probability_mass_function): Refactor the `pmf` file into a definitions file and a constructions file (#10298)
Modified {u}View on Github →2020-10-06 07:07
src/measure_theory/probability_mass_function.lean
lint(measure_theory): docstrings and style (#4455)
Modified {u}View on Github →2020-01-09 21:23
src/data/fin.lean
feat(linear_algebra/multilinear): basics of multilinear maps (#1814) …
Deleted {u}View on Github →2019-04-16 20:12
src/data/fin.lean
feat(*): various additions to low-level files (#904) …
Added {u}View on Github →2019-04-10 17:14
src/measure_theory/probability_mass_function.lean
rename has_sum and is_sum to summable and has_sum (#912)
Modified {u}View on Github →2018-05-29 15:08
analysis/probability_mass_function.lean
feat(analysis): add probability mass functions
Added {u}View on Github →2017-11-24 05:18
data/quot.lean
feat(data/quot): add trunc type (like nonempty in Type) …
Added {u}View on Github →2017-11-22 05:33
data/finset/basic.lean
refactor(data/finset): redefine finsets as subtype of multisets
Deleted {u}View on Github →