submodule

Stream: new members

[亚历山大大帝]

What is the function name for converting ideal I to a submodule?

[Notification Bot]

This topic was moved here from #lean4 > submodule by Yury G. Kudryashov.

[Yury G. Kudryashov]

@czxczx Please ask these questions in the #new members channel. The lean4 channel is for discussions that need the core developers' attention.

[Yury G. Kudryashov]

I : Ideal R is defined as a Submodule R R, so every ideal is a submodule by definition.

[亚历山大大帝]

let I_as_submodule : Submodule R R := I
#check I_as_submodule
apply Submodule.exists_isCompl I_as_submodule Why, although it has been stated that I is Submodule R R, is it still impossible to unify the two types of 'Submodule' and 'Ideal'?

[Aaron Liu]

Is your Ideal an Ideal of a division ring? If it's not then docs#Submodule.exists_isCompl does not apply.

[Aaron Liu]

If it is an ideal of a division ring, then docs#Ideal.eq_bot_or_top says it must be pretty trivial.

[Kevin Buzzard]

Your question would be unambiguous if you asked it as a #mwe . See also #backticks