Mathlib v3 is deprecated. Go to Mathlib v4

Theorem self_adjoint.rat_cast_mem

Modification history

2023-03-08 13:45
src/algebra/star/self_adjoint.lean
feat(algebra/star/self_adjoint): add and generalize trivial lemmas (#18558) …
Deleted self_adjoint.rat_cast_memView on Github →
2022-08-25 03:05
src/algebra/star/self_adjoint.lean
chore(analysis/normed_space/star/*): migrate use of `a ∈ self_adjoint A` to `is_self_adjoint a` (#16212) …
Modified self_adjoint.rat_cast_memView on Github →
2022-07-19 18:28
src/algebra/star/self_adjoint.lean
chore({algebra,data/rat}): use forgetful inheritance for `algebra_rat` (#14894) …
Added self_adjoint.rat_cast_memView on Github →