mathlib3
3fee4b9b - chore(control/random): Move from `system.random.basic` (#10408)

Commit
4 years ago
chore(control/random): Move from `system.random.basic` (#10408) The top folder `system` contains a single file, apparently because it mimics Lean core's organisation. This moves it under `control.` and gets rid of one top folder.
Author
Parents
Loading