for R being Ring
for a being Element of R holds LC (a | R) = a