Algebras where elements have integer norm

Stream: Is there code for X?

[Daniel Weber]

Suppose I have a ring R and a normed field K with Algebra R K. Is there a name for the property "for every x : R, ‖algebraMap R K x‖ is an integer"? Is there a typeclass for that?

[Johan Commelin]

Nope, I don't think so. So you'll have to pass around that property by hand

[Johan Commelin]

But guessing the application you have in mind, maybe you can get away with the norms that are used in number theory

[Daniel Weber]

Could you give some details? I haven't done any number theory in Lean

[Daniel Weber]

Perhaps I could just prove it concretely for Z and C

[Johan Commelin]

Hmmm, you need some sort of triangle inequality

[Riccardo Brasca]

What application do you have in mind?

[Notification Bot]

4 messages were moved from this topic to #mathlib4 > Murty's irreducibility criterion by Johan Commelin.

[Yakov Pechersky]

(deleted)