ideal_quotient): prove dimension of quotient by ideal equals degree of norm of generator (#19121)

Commit

2 years ago

feat(linear_algebra/free_module/ideal_quotient): prove dimension of quotient by ideal equals degree of norm of generator (#19121) Also refactor file into `namespace ideal`. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Author

Multramate

Parents

e1e7190e

mathlib 90b0d53e - feat(linear_algebra/free_module/ideal_quotient): prove dimension of quotient by ideal equals degree of norm of generator (#19121)

mathlib
90b0d53e - feat(linear_algebra/free_module/ideal_quotient): prove dimension of quotient by ideal equals degree of norm of generator (#19121)