Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-14 21:12 c12acedd

View on Github →

feat(algebra/star): star_linear_equiv (#9426)

Estimated changes

Modified src/algebra/ring/comp_typeclasses.lean

added theorem ring_hom_inv_pair.of_ring_equiv

added theorem ring_hom_inv_pair.symm

Modified src/algebra/star/basic.lean

Created src/algebra/star/module.lean

added def star_linear_equiv