mathlib

fa78268d - chore(ring_theory/finiteness): generalize `module.finite.trans` (#18880)

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.