Commit 2021-06-07 04:52 7a21ae17
View on Github →chore(algebra/algebra/subalgebra): make inf and top definitionally convenient (#7812)
This adjusts the galois insertion such that lemma coe_inf (S T : subalgebra R A) : (↑(S ⊓ T) : set A) = S ∩ T := rfl.
It also adds lots of trivial simp lemmas that were missing about the interactions of various coercions and lattice operations.