Commit 2023-04-27 11:18 fa78268d
View on Github →chore(ring_theory/finiteness): generalize module.finite.trans (#18880)
This was stated for algebras but holds more generally for modules.
This now can be used to prove finite_dimensional.trans.
A few downstream proofs were providing the instances arguments explicitly and consequently broke.
Passing those instances via haveI fixes those proofs and makes them less fragile.