lean - 精益：定义 R-ideal 和 R-module 的乘积

Question

我正在尝试学习精益，我正在尝试弄清楚如何I*M = {i*m | i in I, m in M}从理想的 I 和 R 模块 M中创建一个新的 R 模块。

所以我的尝试是首先定义一个映射ideal_mult来创建一个新的 R 模块，然后弄清楚如何为它分配一个好的符号。

import ring_theory.ideals
import algebra.module

universes u v
variables {R : Type u} {M : Type v}
variables [comm_ring R] [add_comm_group M] [module R M]
variables (I: ideal R)

def ideal_mult (I: ideal R) (M: Type v)
        [add_comm_group M] [module R M]: Type v
        :=
    sorry

#check ideal_mult I M

我该如何定义它，以便我可以例如陈述一个假设(h: I*M = M)？

感谢您的帮助！

Answer 1