Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-02 18:42 0393ccbd

View on Github →

feat(ring_theory/algebra): subalgebra_of_subring (#664)

Estimated changes

Modified src/ring_theory/algebra.lean

added def alg_hom_int

deleted def is_ring_hom.to_ℤ_alg_hom

added theorem mem_subalgebra_of_subring

deleted def ring.to_ℤ_algebra

added def subalgebra_of_subring