Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-23 16:33 35ede3d4

View on Github →

chore(algebra/algebra/*): add some simp lemmas (#10969)

Estimated changes

Modified src/algebra/algebra/basic.lean

added theorem alg_equiv.coe_of_bijective

added theorem alg_equiv.of_bijective_apply

Modified src/algebra/algebra/subalgebra.lean

added def algebra.top_equiv

Modified src/field_theory/adjoin.lean

added def intermediate_field.top_equiv

deleted theorem intermediate_field.top_equiv_def

added theorem intermediate_field.top_equiv_symm_apply_coe