Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-01 11:06 17ebcf01

View on Github →

chore(ring_theory/algebra_tower): relax typeclasses (#10078) This generalizes some comm_rings to comm_semirings. Split from #10024

Estimated changes

modified theorem algebra.fg_trans'
modified theorem basis.algebra_map_injective