mathlib3 documentation

lean-ga / for_mathlib.algebra.algebra_operations

Lemmas for algebra/algebra/operations.lean #

source
def submodule.one_eq_algebra_of_id_range {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] :
1 = ⇑subalgebra.to_submodule (algebra.of_id R A).range