Commit 2021-10-22 15:58 29553061

View on Github →

feat(ring_theory/finiteness): generalize module.finite to noncommutative setting (#9860) An almost for free generalization of module.finite to semiring.

Estimated changes

Modified src/ring_theory/finiteness.lean

modified def algebra.finite_presentation

modified theorem module.finite.of_injective

modified theorem module.finite.of_restrict_scalars_finite

modified theorem module.finite.trans

modified theorem module.finite_def