Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-17 07:29 d673e55b

View on Github →

feat(ring_theory/algebra): add ext_iff (#1996)

  • feat(ring_theory/algebra): add ext_iff
  • also add eq_top_iff
  • Update src/ring_theory/algebra.lean

Estimated changes

added theorem algebra.eq_top_iff
added theorem subalgebra.ext_iff