Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-27 22:50 af7a7ee3

View on Github →

feat(ring_theory/algebra): remove of_core

Estimated changes

deleted structure algebra.core
added theorem algebra.mul_smul_comm
deleted def algebra.of_core
modified def algebra.of_subring
deleted theorem algebra.smul_mul
added theorem algebra.smul_mul_assoc
modified def ring.to_ℤ_algebra