local_properties.lean

Commit

3 years ago

Update src/ring_theory/local_properties.lean Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

References

Author

erdOne

Parents