mathlib
a641e1b6 - doc(set_theory/cardinal/basic): tweak documentation (#15480)

Commit
3 years ago
doc(set_theory/cardinal/basic): tweak documentation (#15480) This PR does the following: - remove the mention of `cardinal.min`, as it was removed in #13410. - elaborate on `cardinal.sum`. - add mention of `cardinal.prod`. - separate the documentation of definitions with that of instances.
Author
Parents
Loading