mathlib3
1fef5154 - chore(analysis/normed_space/basic): add short-circuit instance to obtain module structure over reals (#14013)

Commit
3 years ago
chore(analysis/normed_space/basic): add short-circuit instance to obtain module structure over reals (#14013)
Author
Parents
Loading