mathlib
001ba509 - feat(ring_theory/fractional_ideal): `simp` lemmas for `fractional_ideal.canonical_equiv` (#16702)

Commit

3 years ago

feat(ring_theory/fractional_ideal): `simp` lemmas for `fractional_ideal.canonical_equiv` (#16702) Some lemmas I needed for working with the class group of a ring of integers.

Author

Vierkantor

Parents

acd02bbd

mathlib 001ba509 - feat(ring_theory/fractional_ideal): `simp` lemmas for `fractional_ideal.canonical_equiv` (#16702)

mathlib
001ba509 - feat(ring_theory/fractional_ideal): `simp` lemmas for `fractional_ideal.canonical_equiv` (#16702)