mathlib3
ed57bdd3 - feat(number_field): notation for 𝓞 K, an algebra & ∈ 𝓞 K iff (#11476)

Commit

3 years ago

feat(number_field): notation for 𝓞 K, an algebra & ∈ 𝓞 K iff (#11476) From flt-regular.

Author

ericrbg

Parents