Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-25 12:10 34093880

View on Github →

doc(ring_theory/*): add some module docstrings (#3880)

Estimated changes

Modified src/ring_theory/adjoin.lean

Modified src/ring_theory/algebra_operations.lean

Modified src/ring_theory/euclidean_domain.lean

Modified src/ring_theory/free_comm_ring.lean

modified theorem free_comm_ring.coe_lift_hom

modified def free_comm_ring.lift

modified theorem free_comm_ring.lift_comp_of

modified def free_comm_ring.lift_hom

modified theorem free_comm_ring.lift_hom_comp_of

Modified src/ring_theory/free_ring.lean

modified def free_ring.lift

modified theorem free_ring.lift_comp_of

modified def free_ring.lift_hom

Modified src/ring_theory/integral_closure.lean