mathlib3
cc6594a5 - doc(algebra/algebra/basic): Fixes some documentation about `R`-algebras (#4689)

Commit
5 years ago
doc(algebra/algebra/basic): Fixes some documentation about `R`-algebras (#4689) See the associated zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/The.20Type.20of.20R-algebras/near/213722713
Author
Parents
Loading