Haruhisa Enomoto

icon indicating a website link https://haruhisa-enomoto.github.io/

icon location a postdoc majoring in the representation theory of algebras

Results 2 issues of Haruhisa Enomoto

feat(algebra/module/submodule/lattice): `submodule.is_maximal`

3 comment

This PR replaces the previous typeclass for maximal left ideals `ideal.is_maximal : ideal R -> Prop` with `submodule.is_maximal : submodule R M -> Prop`, which is a typeclass for maximal...

delegated
awaiting-CI
too-late

feat(ring_theory/ideal/nc_jacobson_radical): Jacobson radical of noncommutative ring

Define the Jacobson radical of a ring as the intersection of all maximal left ideals, and prove basic properties: famous equivalent conditions for an element in a ring to be...

awaiting-author
too-late