mathlib
18361694 - feat(ring_theory/ideal): Two little `restrict_scalars` lemmas (#16248)

Commit

3 years ago

feat(ring_theory/ideal): Two little `restrict_scalars` lemmas (#16248) I used these two lemmas in one of the definitions of the ideal norm.

Author

Vierkantor

Parents